Level: Lib Thy Top:
Hypotheses:None
Conclusion:
E,T,L:
. Ach,Tor:Signature(E;T;L). w:T.
Run(E;T;L;Ach)
Run(E;T;L;Tor)
Ach 
Tor
IVP(Ach)
Ach.d w = Tor.d w
t0 < w
(w 
Ach.t1 w Tor.t1)
(s:T. t0 s s < w 
(Ach.d s) < (Tor.d s))
Def w
(n:
v:n 
T
t0 = v 0
(i:(n - 1). (v i) < (v (i + 1)))
(i:n. (v i) < w Def (v i) t0 (v i)))
Applied Tactic: UnivCD THENW Auto THEN NSubsetInd 8 THENW Auto
Generated subgoals:1. v:n T
t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < w Def (v i) t0 (v i))2. v:n T
t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < w Def (v i) t0 (v i))