Proof.Propositional

type a /\ b

type a \/ b

type Not a

exfalso

orIntroL

orIntroR

orElim

andIntro

andElimL

andElimR

orAssocL

orAssocR

andAssocL

andAssocR