Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
a:Assignment.
S:Sequent. SqStable(a |
S)
Applied Tactic:
Unfold `sequent_falsifiable` 0 THEN UnivCD THENA Auto
Generated subgoals:
1
. SqStable(
F
S.H.a |= F
F
S.C.a |
F)