proposition: Theorem iff_push_down_forallT : forall A (P Q: A-> [univ]) , (forall a, P a <=> Q a) -> ((forall a, P a) <=> (forall a, Q a)).
proof: Proof. introv Hiff. repeat split; intros; apply Hiff; auto. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega