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

Lemma LRefl: (x:A)(Leq x x). 
Abort. 
Lemma LSymm: (x,y:A)(Leq x y) -> (Leq y x). 
Abort. 

Lemma LTrans: (x,y,z:A)(Leq x y) -> (Leq y z) -> (Leq x z). 
Abort. 

End Leib.

Section Rels.
Variable A:Set.
Variable R:A->A->Prop.
Variable Q:A->A->Prop.
Definition Trans := (x,y,z:A)(R x y) -> (R y z) -> (R x z). 
Definition Subs := (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] (Q: A-> A->Prop) 
(Trans ? Q)-> (Subs ? R Q) -> (Q x y).

Lemma trans_transclos : (Trans ? Trclos).
Abort.

Lemma Subs_rel_transclos : (Subs ? R Trclos). 
Abort. 

End TrClos.

(* Here we prove a variant pf the Knaster Tarski fixed point theorem.
   In Coq, if P:A->Prop, then it is in general _not_ provable that
	P == [x:A](P x)
   because Coq is intensional.
   Therefore we sometimes write [x:A](P x) in stead of P below. *)

Section KnasterTarski. 
Variable A:Set.
Variable Phi :(A->Prop)->(A->Prop).
Definition Sub:= [P,Q:A->Prop](x:A)(P x) ->(Q x).
Definition Mon := (P,Q:A->Prop)(Sub P Q) -> (Sub (Phi P)(Phi Q)).
Axiom PhiMon : Mon.
Definition Closed := [P:A->Prop] (Sub (Phi [x:A](P x)) P).

Definition XX := [x:A](P:A->Prop) (Closed P) -> (P x).
Lemma clos_sub : (P:A->Prop) (Closed P) -> (Sub XX P).
Abort.

Lemma Phi_XX_XX : (Sub (Phi XX) XX).
Abort.

Lemma XX_Phi_XX : (Sub XX (Phi XX)).
Abort.

Definition Weq := [P,Q:A->Prop](Sub P Q)/\(Sub Q P).

Lemma Fix : (Weq XX (Phi XX)).
Abort. 

Lemma Least_Fix : (P:A->Prop)(Closed P)->(Sub XX P).
Abort.

End KnasterTarski.

Section ListTreeInd. 

Variables A, L:Set. 
Variables Nil:L; Cons: A-> L-> L.

(* Variable ListInd : ....... *) 

Variables T,B:Set. 
Variables Leaf:A-> T; Join: B-> T-> T-> T. 
(* Variable TreeInd : ....... *)

End ListTreeInd.