a:Assignment, S:Sequent. SqStable(a |= S)
sq_stable__sequent_satisfiable
F
S.H.a |
F 
FS.C.a |= F
Thm* a:Assignment, S:Sequent. SqStable(a |= S)
sq_stable__sequent_satisfiable
Thm* S:Sequent, a:Assignment. Dec(a |= S)
decidable__sequent_satisfiable