Thms
elimination
Sections
ClassicalProps(jlc)
Doc
fimp
Def
p
q == inr(inr(inr(inr( < p,q > ))))
Thm*
p,q:Formula. p
q
Formula
About:
q == inr(inr(inr(inr( < p,q > ))))
p,q:Formula. pq 
Formulaq == inr(inr(inr(inr( < p,q > ))))
