a |
S }
S:Sequent. Full(S) 
AssignmentS:Sequent, a:Full(S). a |= S a | S
| def | full_sequent_assignment | Full(S) == {a:Assignment| a |= S a | S } |
| THM | full_sequent_assignment_inc | S:Sequent. Full(S) Assignment |
| THM | full_sequent_assignment_properties | S:Sequent, a:Full(S). a |= S a | S |