@[simp, reducible]abbrev Leibniz {A: Type} (x y: A) := ∀ (P: A -> Prop), P x -> P ytheorem Leibniz_refl {A: Type}: ∀ (x: A), Leibniz x x := fun _A _P Px => Pxtheorem Leibniz_trans {A: Type}: ∀ (x y z: A), Leibniz x y -> Leibniz y z  -> Leibniz x z :=        fun _x _y _z Lxy Lyz P Px => Lyz P (Lxy P Px)theorem Leibniz_sym {A: Type}: ∀ (x y: A), Leibniz x y -> Leibniz y x :=  fun x y  Lxy P Py =>      let prop (a: A) := P a -> P x      let proofPropX : prop x := id      let proofPropY: prop y := Lxy prop proofPropX      proofPropY Pytheorem defeq_implies_Leibniz (x y: A) (EQ: x = y):  Leibniz x y := fun P Px => EQ ▸ Pxtheorem Leibniz_implies_defeq (x y: A) (LEQ: Leibniz x y):  x = y := LEQ (fun a => x = a) rfl