Thm* ((Formula List)(Formula List)) Sequent product_inc_Sequent
In prior sections: quot 1 discrete jlc core 3 jlc var jlc assignment
(Formula List)) 
Sequent product_inc_Sequent
T == 
x:S. x 
T
(Formula List)) Sequent product_inc_Sequent