Level: Lib Thy Top: 2
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: RWH (HypC 9) 0 THENA Auto THEN Sel 1 (D 0) THEN Auto
Generated subgoals:

None