+naxiom eq_re : ∀S:Alpha.re S → re S → CProp[0].
+ndefinition RE : Alpha → setoid.
+#A; @(re A); @(eq_re A); ncases admit. nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+alias id "carr" = "cic:/matita/ng/sets/setoids/carr.fix(0,0,1)".
+unification hint 0 ≔ A : Alpha;
+ T ≟ acarr A,
+ P1 ≟ refl ? (eq (RE A)),
+ P2 ≟ sym ? (eq (RE A)),
+ P3 ≟ trans ? (eq (RE A)),
+ X ≟ mk_setoid (re T) (mk_equivalence_relation ? (eq_re A) P1 P2 P3)
+(*-----------------------------------------------------------------------*) ⊢
+ carr X ≡ (re T).
+