proposition: Lemma fold_right_orb_map {T} f (ls : list T) : fold_right orb false (map f ls) = true <-> List.Exists (fun x => f x = true) ls.
proof: Proof. induction ls; repeat match goal with | _ => split | _ => intro | _ => progress simpl in * | [ H : Exists _ [] |- _ ] => solve [ inversion H ] | [ H : Exists _ (_::_) |- _ ] => inversion_clear H | _ => progress split_iff | _ => progress destruct_head sumbool | [ H : (_ || _)%bool = true |- _ ] => apply Bool.orb_true_elim in H | [ H : ?a, H' : ?a -> ?b |- _ ] => specialize (H' H) | [ H : _ = true |- _ ] => rewrite H | [ |- (?a || true)%bool = _ ] => destruct a; reflexivity | _ => solve [ eauto ] | _ => congruence end. 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