Thms
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
fnot
Def
p == inr(inl(p))
Thm*
x:Formula.
x
Formula
About:
p == inr(inl(p))
x:Formula. x 
Formulap == inr(inl(p))
