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
Generated subgoals:

1. v < w v = w