proposition: Lemma umfoldlPtUnE v2 v1 a t (z0 d : R) f : (forall r, a r t v1 = a r t v2) -> um_foldl a z0 d (pts t v1 \+ f) = um_foldl a z0 d (pts t v2 \+ f).
proof: Proof. move=>H. case W : (valid (pts t v1 \+ f)); last first. - move/invalidE: (negbT W)=>->; rewrite umfoldl_undef. rewrite (validPtUnE v2) in W. by move/invalidE: (negbT W)=>->; rewrite umfoldl_undef. elim/um_indf: f z0 W=>[|z0|k v f IH V' P z0 W]; rewrite ?join_undef ?unitR ?umfoldlPt ?(H z0) //. case: (ordP k t) W=>E W; last 2 first. - by move/validAL: W; rewrite (eqP E) (validPtUnE v) validUnEb um_unitbPt. - have D w : all (ord t) (dom (pts k w \+ f)). - apply/allP=>x; rewrite domPtUn inE=>/andP [_] /orP [/eqP <-|] //. by apply: path_mem (@trans K) _; apply: ord_path (@trans K) E P. by rewrite !(umfoldlPtUn a (k:=t)) ?(validPtUnE v1) // H. have D w : all (ord k) (dom (pts t w \+ f)). - apply/allP=>x; rewrite domPtUn inE=>/andP [_] /orP [/eqP <-|] //. by apply: path_mem (@trans K) P. rewrite !(joinCA _ (pts k v)) in W *. rewrite !(umfoldlPtUn a (k:=k)) // ?IH ?(validR W) //. by rewrite joinCA (validPtUnE v1) joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)