Proof is just a () alias -------------------------------------------------

Proof Construction -------------------------------------------------------

trivial is proof by SMT

proof casting | `x *** QED`: x is a proof certificate* strong enough for SMT to prove your theorem | `x *** Admit`: x is an unfinished proof

? is basically Haskell's $ and is used for the right precedence | ? lets you "add" some fact into a proof term

• Checked Proof Certificates ---------------------------------------------

Implicit equality

To summarize:

• (==!) is *only* for proof debugging - (===) does not require explicit proof term
• (?) lets you insert "lemmas" as other Proof values

• Unchecked Proof Certificates -------------------------------------------

The above operators check each intermediate proof step. The operator ==. below accepts an optional proof term argument, but does not check intermediate steps. TODO: What is it USEFUL FOR?

Assumed equality `x ==! y ` returns the admitted proof certificate that result value is equals x and y

• Combining Proof Certificates -------------------------------------------