(* Fill the proofs by replacing "Admitted" by
  a complete proof script, which ends with Qed. *)
Parameter A B C : Prop.

Lemma AimpA : A -> A.
Proof.
Admitted.

Lemma imp_trans : (A -> B) -> (B -> C) -> A -> C.
Proof.
Admitted.

(* What is the computational behaviour illustrated here? *)
Print AimpA.
Print imp_trans.


Lemma and_comm : A /\ B -> B /\ A.
Proof.
Admitted.

Lemma A_nnA : A -> ~ ~ A.
Proof.
(* Observe the definition of negation *)
Unset Printing Notations.
(* Refold default notations *)
Set Printing Notations.
Admitted.

Lemma and_distrib_or :
  (A \/ B) /\ C -> A /\ C \/ B /\ C.
Proof.
Admitted.

Lemma em_equiv :
  (forall A : Prop, A \/ ~A) <-> (forall A : Prop, ~~A -> A).
Proof.
Admitted.

(* Drinker's paradox *)

Parameter Person : Type.
Parameter Drinks : Person -> Prop.

Parameter em : forall A : Prop, A \/ ~A.

Lemma drinker :
  Person -> exists p, Drinks p -> forall p', Drinks p'.
Admitted.

(* Try the same proof using only nnpp (and without using 
its equivalence with em ... *)
Parameter nnpp : forall A:Prop, ~~A -> A.

Lemma drinker' :
  Person -> exists p, Drinks p -> forall p', Drinks p'.
Proof.
intros p.
apply nnpp.
intros h.
Admitted.