Section Leib.
(* Define the Leibniz equality on A *)
Variable A : Set.
Definition Lq (x y : A) := forall P : A -> Prop, P x -> P y.

Lemma LRefl : forall x : A, Lq x x.
Abort.

Lemma LTrans : forall x y z : A, Lq x y -> Lq y z -> Lq x z. 
Abort. 

Lemma LSymm : forall x y : A, Lq x y -> Lq y x.
Abort.
(* There is a surprisingly simple tactic script that proves this.
   Please also inspect and try to understand the generated proof term by typing
   Print LSymm.
*)
End Leib.


Section Rels.
(* Basics about relations *)
Variable A : Set.
Variable R : A -> A -> Prop.
Variable Q : A -> A -> Prop.
Definition Trans := forall x y z : A, R x y -> R y z -> R x z. 
Definition Subs := forall x y : A, R x y -> Q x y.
End Rels.

Section TrClos.
Variable A : Set.
Variable R : A -> A -> Prop.

Definition Trclos (x y : A) :=
  forall Q : A -> A -> Prop, Trans _ Q -> Subs _ R Q -> Q x y.
(* Note the use of _ which is a place holder for an argument 
   to be inferred by the type checker *)

(* Prove that the transitive closure is transitive *)
Lemma trans_transclos : Trans _ Trclos.
Abort.


(* Prove that the transitive closure contains R *)
Lemma Subs_rel_transclos : Subs _ R Trclos. 
Abort.

End TrClos.


Section Existential.

Definition exi (A:Set)(P:A->Prop) := forall B:Prop, (forall x:A, P x -> B) -> B.

Variable A:Set.
Variable P: A -> Prop.
Variable C:Prop.

Lemma ex_intro : forall a:A, P a -> exi A P.
Abort.

Lemma ex_elim : exi A P -> (forall x:A, P x -> C) -> C.
Abort.

End Existential.