Axiom FOTerm : Type.
Axiom FOFormula : Type.
Axiom fo_bot : FOFormula.
Axiom fo_top : FOFormula.
Axiom fo_not : FOFormula -> FOFormula.
Axiom fo_and : FOFormula -> FOFormula -> FOFormula.
Axiom fo_or : FOFormula -> FOFormula -> FOFormula.
Axiom fo_impl : FOFormula -> FOFormula -> FOFormula.
Axiom fo_iff : FOFormula -> FOFormula -> FOFormula.
Axiom fo_forall : nat -> FOFormula -> FOFormula.
Axiom fo_exists : nat -> FOFormula -> FOFormula.

(** * Pretty printer for FOL *)

Declare Custom Entry FOL.

Notation "[ e ]" := e (e custom FOL at level 0).

Notation "( x )" := x (in custom FOL, x at level 2).

Notation "x" := x (in custom FOL at level 0, x ident).

Notation "⊥" := fo_bot
  (in custom FOL at level 0).
Notation "⊤" := fo_top
  (in custom FOL at level 0).
Notation "¬ A" := (fo_not A)
  (in custom FOL at level 35,
    right associativity, format "'¬' A").
Infix "∧" := fo_and
  (in custom FOL at level 40,
    left associativity).
Infix "∨" := fo_or
  (in custom FOL at level 50,
    left associativity).
Infix "→" := fo_impl
  (in custom FOL at level 99,
    right associativity).
Infix "↔" := fo_iff
  (in custom FOL at level 95,
    right associativity).
Notation "∀ x A" := (fo_forall x A)
  (in custom FOL at level 120,
    left associativity).
Notation "∃ x A" := (fo_exists x A)
  (in custom FOL at level 120,
    left associativity).

(* Print fo_sub. *)

Section Check.
  Context (A B : FOFormula) (x : nat).
  Goal Type.
  pose [ ¬(¬¬¬¬ A ∧ B) → A ∨ B ∧ A ↔ ∀ x A ].
  pose [A ∨ A].
  Admitted.
  Check [A ∨ A].
End Check.