Thm* S:Sequent, a:Full(S). a |= S a | S full_sequent_assignment_properties

Thm* S:Sequent. Full(S) Assignment full_sequent_assignment_inc