proposition: Lemma fst_fold_right {A B A'} (f : B -> A -> A) (g : B -> A * A' -> A') a a' ls : fst (fold_right (fun b aa' => (f b (fst aa'), g b aa')) (a, a') ls) = fold_right f a ls.
proof: Proof. induction ls; simpl; trivial. rewrite IHls; reflexivity. Qed.
imports: Coq.Lists.List Coq.ZArith.ZArith Coq.Lists.SetoidList Coq.Setoids.Setoid Coq.Classes.RelationClasses Coq.Program.Program Coq.Classes.Morphisms Fiat.Common.Tactics.SplitInContext Fiat.Common.Tactics.Combinators Fiat.Common.Tactics.FreeIn Fiat.Common.Tactics.SetoidSubst Fiat.Common.Tactics.BreakMatch Fiat.Common.Tactics.Head Fiat.Common.Tactics.FoldIsTrue Fiat.Common.Tactics.SpecializeBy Fiat.Common.Tactics.DestructHyps Fiat.Common.Tactics.DestructSig Fiat.Common.Tactics.DestructHead Fiat.Common.Coq__8_4__8_5__Compat