G:Sequent.
L:Sequent List.
s
L.(
(s) = 0)
& (sL.|= s 
|= G )
& (a:Assignment. sL.a |
s a | G)
normalization_lemma
S == FS.H.a |= F & FS.C.a | F
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 falsification sequent sat lemmas full sequent assignment elimination