proposition: Lemma first_index_helper_default_map {A' A B} (rect : forall A, option (nat * A) -> B) (rec : forall A, nat * A -> nat * A) (test : A -> bool) (f : A' -> A) (ls : list A') (rectNone : rect A None = rect A' None) (rectSome : forall n x, rect A (Some (rec _ (n, f x))) = rect A' (Some (rec _ (n, x)))) : Operations.List.first_index_helper test (rect _) (List.map f ls) (rec _) = Operations.List.first_index_helper (fun x => test (f x)) (rect _) ls (rec _).
proof: Proof. revert dependent rec; induction ls as [|x xs IHxs]; simpl; intros; [ apply rectNone | ]. specialize (IHxs (fun _ x0 => rec _ (S (fst x0), snd x0))); simpl in *. rewrite IHxs by eauto; clear IHxs. destruct (test (f x)); simpl; [ | reflexivity ]. apply rectSome. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts