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

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