Level: Lib Thy Top: 2
Hypotheses:

  1. T :

  2. R : T T

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

  4. n :

  5. 2 < n

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

Conclusion:

v:n T. (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1))

Applied Tactic: D 0 THENW Auto THEN With v (D 6) THENW Auto THEN D 0 THENW Auto THEN D 7 THENW Auto
Generated subgoals:

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

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