proposition: Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
proof: Proof. split; [induction 1; inv 1; auto|]. intros Hin; induction l as [|x l IH]; constructor; [apply Hin; constructor|]. apply IH. intros ??. apply Hin. by constructor. Qed.
imports: stdpp(options)