Thm* F:Formula. |= F |= < nil,[F] > formula_valid_iff_sequent_valid

In prior sections: formula valuation formula satisfaction formula falsification formula rank formula equality sat lemmas full assignment formula validity sequent formula list sequent rank