proposition: Lemma fold_right_projT1 {A B X} (P : A -> Type) (init : A * B) (ls : list X) (f : X -> A -> A) (g : X -> A -> B -> B) pf pf' : List.fold_right (fun (x : X) (acc : A * B) => (f x (fst acc), g x (fst acc) (snd acc))) init ls = let fr := List.fold_right (fun (x : X) (acc : sigT P * B) => (existT P (f x (projT1 (fst acc))) (pf' x acc), g x (projT1 (fst acc)) (snd acc))) (existT P (fst init) pf, snd init) ls in (projT1 (fst fr), snd fr).
proof: Proof. revert init pf. induction ls; simpl; intros [? ?]; trivial; simpl. intro. simpl in *. erewrite IHls; simpl. 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