S:Sequent, a:Full(S). a |= S 
a |
S
full_sequent_assignment_properties
S == F
S.H.a |= F & FS.C.a | F
Thm* S:Sequent, a:Full(S). a |= S a | S
full_sequent_assignment_properties
In prior sections: sequent falsification sequent sat lemmas