Variable T : Set.
Variable A : T -> Prop.
Variable B : Prop.
Variable T_nonempty : T.
Definition lhs
:= (exists x, A x) -> B.
Definition rhs
:= forall x, (A x -> B).
Theorem dir_b
: rhs -> lhs.
Proof.
unfold lhs. unfold rhs. intros HA HE.
inversion HE. apply HA with x. apply H.
Qed.
Theorem dir_a
: lhs -> rhs.
Proof.
unfold lhs. unfold rhs. intros HE x HA.
apply HE. exists x. apply HA.
Qed.
Theorem both
: lhs <-> rhs.
Proof.
unfold iff. split. apply dir_a. apply dir_b.
Qed.