DISP	formula_sat_df	<a:Assignment:L> |= <F:Formula:L> == <a> |= <F>
ABS	formula_sat	a |= F == (F under a) = 3
THM	formula_sat_wf	a:Assignment. F:Formula. a |= F
THM	sq_stable__formula_sat	a:Assignment. F:Formula. SqStable(a |= F )
THM	decidable__formula_sat	a:Assignment. f:Formula. Dec(a |= f )

the other theories