Reimplementing a subset of Coq in Python
First order logic:
Theorem test : exists x : nat, x + 2 = 4. Theorem test2 : forall y : nat, (exists x : nat, x = y).
Second order logic (quantifing over first order logic statements):
forall y : (fun x : nat -> nat)
Higher order logic...so on and so forth