proposition: Lemma fold_right_and_True_map {A} {P : A -> Prop} {ls : list A} : List.fold_right and True (List.map P ls) <-> (forall x, List.In x ls -> P x).
proof: Proof. rewrite fold_right_and_True; split; intros H x Hx. { apply H, List.in_map, Hx. } { apply List.in_map_iff in Hx. destruct Hx as [? [? ?]]; subst; eauto. } Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat