PrintForm Definitions formula falsification Sections ClassicalProps(jlc) Doc

At: sq stable formula falsifiable

a:Assignment, F:Formula. SqStable(a | F)
By:
Repeat (Unfolds [`formula_falsifiable`;`sq_stable`;`squash`] 0)
THEN
UnivCD
Generated subgoal:

11. a: Assignment
2. F: Formula
3. {True| (F under a) = 3}
(F under a) = 3

About:
allequal