An impredicative definition of equality

Section leibniz.
 Variable A : Set.
 
 Set Implicit Arguments.

 Definition leibniz (a b:A) : Prop := forall P:A -> Prop, P a -> P b.

 Theorem leibniz_sym : symmetric A leibniz.

 Theorem leibniz_refl : reflexive A leibniz. 

 Theorem leibniz_trans :  transitive A leibniz.

 Theorem leibniz_equiv : equiv A leibniz.

 Theorem leibniz_least :
  forall R:relation A, reflexive A R -> inclusion A leibniz R.

 Theorem leibniz_eq : forall a b:A, leibniz a b -> a = b.

 Theorem eq_leibniz : forall a b:A, a = b -> leibniz a b.

 Theorem leibniz_ind :
  forall (x:A) (P:A -> Prop), P x -> forall y:A, leibniz x y -> P y.

Solution

• leibniz.v
• Alternate solution, using RelationClasses