proposition: Lemma helper2 p h1 h2 z0 k v : growing (h1 \+ (k \-> v \+ h2)) -> valid (h1 \+ (k \-> v \+ h2)) -> {in dom h1, forall x, x < k} -> all (ord k) (dom h2) -> p (k, v) -> f (evalv a p (h1 \+ (k \-> v \+ h2)) z0) = f z0 -> f (a (evalv a p h1 z0) v) = f (evalv a p h1 z0).
proof: Proof. move=>G W D1 D2 P E1; rewrite evalUn ?W // in E1; last first. - move=>x y /D1 X1; rewrite domPtUn inE (validR W). by case/orP=>[/eqP <-|/(allP D2)] //; apply: ltn_trans. suff E2 : f (evalv a p h1 z0) = f z0. - by apply: helper1 (growR W G) (validR W) D2 P _; rewrite E1 E2. apply/eqP; case: ordP=>//. - by move: (helper0 p z0 (growL W G)); rewrite /oleq eq_sym; case: ordP. move: (helper0 p (evalv a p h1 z0) (growR W G)). by rewrite -E1 /oleq eq_sym; case: ordP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)