normalization Sections ClassicalProps(jlc) Doc

Def p == inr(inl(p))

In prior sections: sat lemmas elimination