proposition: Lemma fold_right_beq_in_correct ls : List.fold_right (fun y else_case => If beq y x Then f y Else else_case) base ls = (if list_bin beq x ls then f x else base).
proof: Proof. induction ls as [|y ys IHys]. { simpl; reflexivity. } { simpl; rewrite IHys; clear IHys. destruct (beq y x) eqn:Heq; simpl. { apply bl in Heq; subst. rewrite Bool.orb_true_r; reflexivity. } { rewrite Bool.orb_false_r; 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