-(*
-definition Leibniz: Type → setoid.
- intro;
- constructor 1;
- [ apply T
- | constructor 1;
- [ apply (λx,y:T.cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y)
- | alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
- apply refl_eq
- | alias id "sym_eq" = "cic:/matita/logic/equality/sym_eq.con".
- apply sym_eq
- | alias id "trans_eq" = "cic:/matita/logic/equality/trans_eq.con".
- apply trans_eq ]]
-qed.
-
-coercion Leibniz.
-*)
-