Level:
Lib
Thy
Top
:
4
Hypotheses:
E :
T :
L :
S : Signature(E;T;L)
u : T
v : T
w : T
Run(E;T;L;S)
u = v
v = w
Conclusion:
u < w
u = w
Applied Tactic:
Sel 2 (D 0) THEN Auto
Generated subgoals:
None