proposition: Lemma fold_right_push_iff' {A} (f : A -> A -> A) (g : Prop -> Prop -> Prop) (Q : A -> Prop) (x : A) xs (Hfg : forall x y, Q (f x y) <-> g (Q x) (Q y)) {g_Proper : Proper (iff ==> iff ==> iff) g} : Q (fold_right f x xs) <-> fold_right g (Q x) (List.map Q xs).
proof: Proof. apply fold_right_push_iff; try assumption. exact _. 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