Intuitionistic Logic: propositional logic.
(F⇒A), (A⇒T), (A⇒A).

Intuitionistic Logic: a prenex operation for ∃.
(∃x.P(x)∧∃y.Q(y))⇒∃x.∃y.(P(x)∧Q(y))

Intuitionistic Logic: if a satisfies ∀y.P(a,y), then a satisfies P(a,b)∧P(a,c).
(∃x.∀y.P(x,y)⇒∃x.(P(x,b)∧P(x,c)))

Intuitionistic Logic: Intuitionistic double negation.
(∃x.P(x)⇒¬¬∃x.P(x))

Intuitionistic Logic: Excluded Middle is not false.
∀x.¬¬(∃y.P(x,y)∨¬∃y.P(x,y))

Intuitionistic Logic: identity.
(∃x.∀y.∃z.P(x,y,z)   ⇒   ∃x.∀y.∃z.P(x,y,z))

Intuitionistic Logic: double negation for a simply universal formula.
(¬¬∀x.P(x)⇒∀x.P(x))

Intuitionistic Logic: f function and fg injective imply g injective.
( Fun_f∧Inj_fg ⇒ Inj_g )