proposition: Lemma pull_forall_iff {A} (P Q : A -> Prop) : (forall x : A, (P x <-> Q x)) -> ((forall x : A, P x) <-> (forall x : A, Q x)).
proof: Proof. firstorder eauto. Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat