Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. R : T T

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

  4. n :

  5. 0 < n

  6. 2 = n

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 0 (D 0) THENW Auto THEN With 0 (D 8) THENW Auto THEN Assert 0 + 1 = n - 1 THENA Auto THEN RWH (HypC 9) 8 THEN Auto
Generated subgoals:

None