proposition: Lemma fold_right_and_True {ls : list Prop} : List.fold_right and True ls <-> (forall P, List.In P ls -> P).
proof: Proof. split; induction ls; simpl in *; repeat (subst || intros [] || intro); repeat split; try assumption; try apply IHls; intros; eauto; match goal with | [ H : _ |- _ ] => apply H; solve [ left; reflexivity | right; assumption ] end. Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat