--- Leibnitz Equality

( LEQ := [U : Type][x,y : U] {P : U -> Prop}(P x) -> (P y) )

--- Equivalence of Polymorphic Equality and Leibnitz Equality

( EQ_implies_LEQ : {U : Type}{x,y : U} (x = y) -> (LEQ ? x y) )

( LEQ_implies_EQ : {U : Type}{x,y : U} (LEQ ? x y) -> (x = y) )

--- Some Properties

( EQ_is_reflexive : {U : Type}{x : U} (x = x) )

( EQ_is_symmetric : {U : Type}{x,y : U} (x = y) -> (y = x) )

( EQ_is_transitive : {U : Type}{x,y,z : U} (x = y) -> (y = z) -> (x = z) )
 
--- Built-in Extensionality

( EXT : {T : Type}{C : T -> Type}{f,g : {x : T}(C x)}
  {x : T}((f x) = (g x)) -> (f = g) )

( done )