Exercises
- Symmetry : a:(), b:(); a=b|- b=a
- Transitivity: a:(), b:(), c:(); a=b, b=c |- a=c
- Leibniz: P ::(), a:(); P(a) |- forall x:(). x=a -> P(x)
- Dual: P ::(), a:(); forall x:(). x=a -> P(x) |- P(a)
- Basic algebra: type A, type B, f : A->B, g : B -> A; forall y:B.f(g(y)) = y , forall x:A. exists y:B. x = g(y)|- forall x:A.g(f(x)) = x