∃x : ℤ. x > 3 : Prop
∃x : ℚ. x > 3 : Prop
∃x : ℕ, y : ℕ. x > y : Prop
∃x : ℕ. ∃y : ℕ. x > y : Prop
∀x : ℕ, y : ℕ, z : ℕ. x + y + z == x + (y + z) : Prop
∃x : ℕ. ∀y : ℕ. x <= y : Prop
not(∀x : Bool. true \/ x) : Prop
(∀x : Void. false) /\ true : Prop
(∀x : Void. false) \/ true : Prop