formula satisfaction Sections ClassicalProps(jlc) Doc

Def SqStable(P) == P P

Thm* a:Assignment, F:Formula. SqStable(a |= F ) sq_stable__formula_sat

In prior sections: core fun 1 rel 1 quot 1 core 3 jlc list 3 jlc