proposition: Lemma first_index_default_map {A B} (test : B -> bool) (f : A -> B) (ls : list A) (default : nat) : Operations.List.first_index_default test default (List.map f ls) = Operations.List.first_index_default (fun x => test (f x)) default ls.
proof: Proof. unfold Operations.List.first_index_default in *. rewrite (@first_index_helper_default_map _ _ _ (fun _ => option_rect (fun _ => nat) (@fst _ _) default) (fun _ x => x)) by reflexivity. reflexivity. 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