sat lemmas Sections ClassicalProps(jlc) Doc

Def pq == inr(inr(inr(inl( < p,q > ))))

Thm* a:Assignment, q,r:Formula. a | qr a | q & a | r formula_or_falsifiable_lemma

Thm* a:Assignment, q,r:Formula. a |= qr a |= q a |= r formula_or_sat_lemma