Proof.QED

data QED a

qed

imports

decl

data Laws

law

laws

data Proof a

type PropString

prove

data Bind a

satisfy

bind

rhs

lhs

bhs

at

recurse

unfold

unfold_

strict

expand

unlet

divide

twice

thrice

many

perhaps

skip

qedCheat

unsafeCheat