Level: Lib Thy Top:
Hypotheses:None
Conclusion:
E,T,L:
. Ach,Tor:Signature(E;T;L). u,w:T.
Run(E;T;L;Ach)
Run(E;T;L;Tor)
Ach 
Tor
IVP(Ach)
Ach.d w = Tor.d w
t0 
u
u < w
(w Ach.t1 w Tor.t1)
(Ach.d u) < (Tor.d u)
Def u
Def w
(
v:T. u < v v < w Def v)
Applied Tactic: Auto THEN Unfold `ivp` 11 THEN InstHyp [
u
;w;Tor.d u] 11 THENA Auto
Generated subgoals:1. (Tor.d u) < (Ach.d w)2. Def (Tor.d u)
3. v:T. u < v v < w Def v