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