At: discrete Sequent 1
1. Discrete{Formula}
Discrete{Sequent}
By:
Unfold `Sequent` 0
THEN
BackThru
Thm* 
T1:Type{i}, T2:Type{j}.
Discrete{T1} 
Discrete{T2} Discrete{(T1
T2)}
THEN
Using [`T',Formula]
(BackThru
Thm* Discrete{T} Discrete{(T List)})
THEN
Trivial
Generated subgoals:None