proposition: Lemma umfoldlUnPtE v2 v1 a t (z0 d : R) f : (forall r, a r t v1 = a r t v2) -> um_foldl a z0 d (f \+ pts t v1) = um_foldl a z0 d (f \+ pts t v2).
proof: Proof. by rewrite !(joinC f); apply: umfoldlPtUnE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)