proposition: Lemma fold_right_orb b ls : fold_right orb b ls = true <-> fold_right or (b = true) (map (fun x => x = true) ls).
proof: Proof. induction ls; simpl; intros; try reflexivity. rewrite <- IHls; clear. repeat match goal with | _ => assumption | _ => split | _ => intro | _ => progress subst | _ => progress simpl in * | _ => progress destruct_head or | _ => progress destruct_head bool | _ => left; reflexivity | _ => right; assumption 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