normalization
Sections
ClassicalProps(jlc)
Doc
Def
p
q == inr(inr(inr(inl( < p,q > ))))
In prior sections:
sat
lemmas
elimination
q == inr(inr(inr(inl( < p,q > ))))