Reimplementing a subset of Coq in Python
Just kidding, Coq is too complex. We implemented metamath instead.
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