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