Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. R : T T

  3. n : {2...}

  4. v : n T

  5. Trans(T;x,y.x R y)

  6. i:(n - 1). (v i) R (v (i + 1))

Conclusion:

(v 0) R (v (n - 1))

Applied Tactic: 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))