Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

E,T,L:. S:Signature(E;T;L). u,v,w:T. Run(E;T;L;S) u v v w u w

Applied Tactic: Unfold `sign_t_ref_rel` 0 THEN Reduce 0 THEN Auto THEN D 10 THEN D 9
Generated subgoals:

1. u < w u = w

2. u < w u = w

3. u < w u = w

4. u < w u = w