proposition: Lemma helper1 p h z0 k v : growing (k \-> v \+ h) -> valid (k \-> v \+ h) -> all (ord k) (dom h) -> p (k, v) -> f (evalv a p (k \-> v \+ h) z0) = f z0 -> f (a z0 v) = f z0.
proof: Proof. move=>G W D P; move: (growR W G)=>Gh. have K: (k, v) \In k \-> v \+ h by apply/InPtUnE=>//; left. rewrite evalPtUn // P => E; apply/eqP; case: ordP=>//. - by move/(G k v z0): K; rewrite /oleq eq_sym; case: ordP. by move: (helper0 p (a z0 v) Gh); rewrite -E /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)