Proof.Propositional

type a /\ b

type a \/ b

type Not a

exfalso

orIntroL

orIntroR

orElim

andIntro

andElimL

andElimR

orAssocL

orAssocR

andAssocL

andAssocR

data IsTrue b

class Empty a

withEmpty

withEmpty'

refute

class Inhabited a

withInhabited

prove