Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. R:T 
T 
. n:{2...}. v:
n T.
Trans(T;x,y.x R y) 
(i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1))
Applied Tactic: UnivCD THENW Auto THEN NSubsetInd 3 THENW Auto
Generated subgoals:1. v:n T. (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1))2. v:n T. (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1))