proposition: Lemma fold_right_andb_map_impl {T} x y f g (ls : list T) (H0 : x = true -> y = true) (H1 : forall k, f k = true -> g k = true) : (fold_right andb x (map f ls) = true -> fold_right andb y (map g ls) = true).
proof: Proof. induction ls; simpl; intros; try tauto. rewrite IHls; simpl; repeat match goal with | [ H : _ = true |- _ ] => apply Bool.andb_true_iff in H | [ |- _ = true ] => apply Bool.andb_true_iff | _ => progress destruct_head and | _ => split | _ => auto 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