{A B : Type} (f : B -> A -> A) (i : A) (l l' : list B) : fold_right f i (l ++ l') = fold_right f (fold_right f i l') l. Proof. induction l in i |- *. 1: reflexivity. exact (ap (f a) (IHl _)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum