proposition: Lemma foldr_ext {A B} (f1 f2 : B → A → A) x1 x2 l1 l2 : (∀ b a, f1 b a = f2 b a) → l1 = l2 → x1 = x2 → foldr f1 x1 l1 = foldr f2 x2 l2.
proof: Proof. intros Hf -> ->. induction l2 as [|x l2 IH]; f_equal/=; by rewrite Hf, IH. Qed.
imports: stdpp(options)