proposition: Lemma growEn h t1 t2 z0 k v : growing a f h -> (k, v) \In h -> t1 < k <= t2 -> f (exec a t2 h z0) = f (exec a t1 h z0) -> f (a (exec a k.-1 h z0) v) = f (exec a k.-1 h z0).
proof: Proof. by apply: growE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)