Thm* S:Sequent. |= S Type sequent_valid_wf

In prior sections: sequent sequent equality sequent rank sequent satisfaction sequent falsification sequent sat lemmas full sequent assignment