Lemma l1x:
forall P Q, P -> (P -> Q) -> Q.
Proof.
auto.
Qed.
Definition l1 :=
fun P Q (p : P) (f : P -> Q) => f p.
Lemma l2x:
forall P Q : Prop, (P -> Q) -> ~Q -> ~P.
Proof.
auto.
Qed.
Definition l2 :=
fun P Q (f : P -> Q) (a : Q -> False)
(b : P) => a (f b).
Axiom xm:
forall R, R \/ ~R.
Lemma l3:
forall P Q : Prop,
(P -> Q) /\ (~P -> Q) -> Q.
Proof.
intros P Q [H1 H2].
destruct xm with P;
[apply H1 | apply H2]; assumption.
Qed.
Lemma dnegx:
forall P : Prop, P -> ~~P.
Proof.
intros P p H.
apply H.
assumption.
Qed.
Lemma dneg:
forall P, ~~P -> P.
Proof.
intros P H.
destruct xm with P.
assumption.
destruct (H H0).
Qed.