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