PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: formula falsifiable lemma1 1
1. a: Assignment
2. F: Formula
3. a | F

a |= F
By:
Unfold `not` 0
THEN
Unfold `formula_sat` 0
THEN
Unfold `formula_falsifiable` 3
Generated subgoal:

13. (F under a) = 3
4. (F under a) = 3
False

About:
false