proposition: Lemma fusion_foldr {T R Q} (g : R -> Q) f0 f1 z0 z1 (xs : seq T) : (forall x y, g (f0 x y) = f1 x (g y)) -> g z0 = z1 -> g (foldr f0 z0 xs) = foldr f1 z1 xs.
proof: Proof. by move=>Hf Hz; elim: xs=>//= x xs <-. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)