codepad
[
create a new paste
]
login
|
about
Language:
C
C++
D
Haskell
Lua
OCaml
PHP
Perl
Plain Text
Python
Ruby
Scheme
Tcl
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.
Private
[
?
]
Run code
Submit