sat lemmas Sections ClassicalProps(jlc) Doc

Def p == inr(inl(p))

Thm* F:Formula, a:Assignment. a | F a |= F formula_not_falsifiable_lemma

Thm* F:Formula, a:Assignment. a |= F a | F formula_not_sat_lemma