DISP	sequent_satisfiable_df	<a:Assignment:L> |= <S:Sequent:L>== <a> |= <S>
ABS	sequent_satisfiable	a |= S == FS.H.a | F FS.C.a |= F
THM	sequent_satisfiable_wf	a:Assignment. S:Sequent. a |= S
THM	decidable__sequent_satisfiable	S:Sequent. a:Assignment. Dec(a |= S)
THM	sq_stable__sequent_satisfiable	a:Assignment. S:Sequent. SqStable(a |= S)

the other theories