PROOF.bend checks

PROOF.bend -- the gate. bend PROOF.bend fails while any law is open or false, and prints "All terms check." once every one of them holds.

There are no tactics: a proposition is a type, a proof is a def of that type. {==} proves {a == b : T} when both sides compute to the same term %e : P rewrites with e : {a == b : T}; P is the goal with _ marking b a recursive call IS the induction hypothesis