TaPL24章のネタです。まずStatementがcoqで正しく書けているか怪しいですが…
Theorem exists_forall_second: forall T: Prop -> Prop, ((exists X, T X) <-> (forall Y: Prop, (forall X, T X -> Y) -> Y)). intros. split. - intros. destruct H. now apply H0 in H. - intros. apply H. intros. now exists X. Qed.