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))