Thm* G:Sequent. L:Sequent List. sL.((s) = 0) & (sL.|= s |= G ) & (a:Assignment. sL.a | s a | G) normalization_lemma

In prior sections: assignment valuation formula satisfaction formula falsification sat lemmas sequent satisfaction sequent falsification sequent sat lemmas full sequent assignment elimination