Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
a:Assignment.
F:Formula. SqStable(a |= F )
Applied Tactic:
Unfold `sq_stable` 0 THEN Unfold `formula_sat` 0 THEN Auto
Generated subgoals:
1
. (F under a) = 3