Level: Lib Thy Top: 1
Hypotheses:

  1. E :

  2. T :

  3. L :

  4. S : Signature(E;T;L)

  5. u : T

  6. v : T

  7. w : T

  8. Run(E;T;L;S)

  9. u < v

  10. v < w

Conclusion:

u < w u = w

Applied Tactic: Sel 1 (D 0) THENA Auto THEN Unfold `run` 8 THEN D 8 THEN D 9 THEN Thin 10 THEN Unfold `ir_linorder` 9 THEN D 9 THEN Unfold `ir_order` 10 THEN D 10 THEN Unfold `trans` 11 THEN InstHyp [ u;v;w] 11 THEN Auto
Generated subgoals:

None