Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

a:Assignment. F:Formula. SqStable(a | F)

Applied Tactic: Repeat (Unfolds ``formula_falsifiable sq_stable squash`` 0) THEN UnivCD THENA Auto
Generated subgoals:

1. (F under a) = 3