二階命題論理の存在量化子を全称量化子で書き換える

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.