proposition: Lemma forall_iff: forall {A: Type} P Q, (forall x: A, P x <-> Q x) -> ((forall x, P x) <-> (forall x, Q x)).
proof: Proof. intros. firstorder. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Program.Basics