proposition: Lemma iff_under_forall {X} (P Q: X -> Prop): (forall x, P x <-> Q x) -> ((forall x, P x) <-> (forall x, Q x)).
proof: Proof. firstorder. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid