Level: Lib Thy Top: 1
Hypotheses:

  1. E :

  2. T :

  3. L :

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

  5. Tor : Signature(E;T;L)

  6. u : T

  7. w : T

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

  9. Run(E;T;L;Tor)

  10. Ach Tor

  11. IVP(Ach)

  12. Ach.d w = Tor.d w

  13. t0 u

  14. u < w

  15. w Ach.t1

  16. w Tor.t1

  17. (Ach.d u) < (Tor.d u)

  18. Def u

  19. Def w

Conclusion:

v:T. u < v v < w Def v

Applied Tactic: Unfold `ivp` 11
Generated subgoals:

1. v:T. u < v v < w Def v