Thm* S:Sequent. Full(S) Assignment full_sequent_assignment_inc
In prior sections: quot 1 discrete jlc core 3 jlc var jlc assignment sequent
S:Sequent. Full(S) 
Assignment
full_sequent_assignment_inc
T == x:S. x 
T
S:Sequent. Full(S) Assignment
full_sequent_assignment_inc