DISP	sequent_valid_df	|= <S:Sequent:L> == |= <S>
ABS	sequent_valid	|= S == a:Full(S). a |= S
THM	sequent_valid_wf	S:Sequent. |= S
THM	formula_valid_iff_sequent_valid	F:Formula. |= F |= <[], F::[]>

the other theories