Proof.QED.Advanced

data Known

getKnown

data Unknown

getUnknown

data Goal

getGoal

data BadProof

badProof

isBadProof

data Laws

rewriteUnfold

rewriteEquivalent

rewriteRecurse

rewriteSplit

rewriteTautology