+ndefinition RE : Alpha → setoid.
+#A; @(re A); @(eq_re A);
+##[ #p; nelim p; /2/;
+##| #p1; nelim p1; ##[##1,2: #p2; ncases p2; /2/;
+ ##|##2,3: #x p2; ncases p2; /2/;
+ ##|##4,5: #e1 e2 H1 H2 p2; ncases p2; /3/; #e3 e4; *; #; @; /2/;
+ ##|#r H p2; ncases p2; /2/;##]
+##| #p1; nelim p1;
+ ##[ ##1,2: #y z; ncases y; ncases z; //; nnormalize; #; ncases (?:False); //;
+ ##| ##3: #a; #y z; ncases y; ncases z; /2/; nnormalize; #; ncases (?:False); //;
+ ##| ##4,5: #r1 r2 H1 H2 y z; ncases y; ncases z; //; nnormalize;
+ ##[##1,3,4,5,6,8: #; ncases (?:False); //;##]
+ #r1 r2 r3 r4; nnormalize; *; #H1 H2; *; #H3 H4; /3/;
+ ##| #r H y z; ncases y; ncases z; //; nnormalize; ##[##1,2,3: #; ncases (?:False); //]
+ #r2 r3; /3/; ##]##]
+nqed.
+
+unification hint 0 ≔ A : Alpha;
+ S ≟ acarr A,
+ T ≟ carr S,
+ P1 ≟ refl ? (eq0 (RE A)),
+ P2 ≟ sym ? (eq0 (RE A)),
+ P3 ≟ trans ? (eq0 (RE A)),
+ X ≟ mk_setoid (re T) (mk_equivalence_relation ? (eq_re A) P1 P2 P3)
+(*-----------------------------------------------------------------------*) ⊢
+ carr X ≡ re T.
+
+unification hint 0 ≔ A:Alpha, a,b:re (carr (acarr A));
+ R ≟ eq0 (RE A),
+ L ≟ re (carr (acarr A))
+(* -------------------------------------------- *) ⊢
+ eq_re A a b ≡ eq_rel L R a b.
+
+(* XXX This seems to be a pattern for equations in setoid(0) *)
+unification hint 0 ≔ AA;
+ A ≟ carr (acarr AA),
+ R ≟ setoid1_of_setoid (RE AA)
+(*-----------------------------------------------*) ⊢
+ re A ≡ carr1 R.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
+unification hint 0 ≔ S : Alpha, x,y: re (carr (acarr S));
+ SS ≟ RE S,
+ TT ≟ setoid1_of_setoid SS,
+ T ≟ carr1 TT
+(*-----------------------------------------*) ⊢
+ eq_re S x y ≡ eq_rel1 T (eq1 TT) x y.
+
+(* contructors are morphisms *)
+nlemma c_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
+#A; napply (mk_binary_morphism … (λs1,s2:re A. s1 · s2)); #a; nelim a; /2/ by conj; nqed.
+
+(* XXX This is the good format for hints about morphisms, fix the others *)
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
+unification hint 0 ≔ S:Alpha, A,B:re (carr (acarr S));
+ SS ≟ carr (acarr S),
+ MM ≟ mk_unary_morphism ?? (λA.
+ mk_unary_morphism ??
+ (λB.A · B) (prop1 ?? (fun1 ?? (c_is_morph S) A)))
+ (prop1 ?? (c_is_morph S)),
+ T ≟ RE S
+(*--------------------------------------------------------------------------*) ⊢
+ fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ c SS A B.
+
+nlemma o_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
+#A; napply (mk_binary_morphism … (λs1,s2:re A. s1 + s2)); #a; nelim a; /2/ by conj; nqed.
+
+unification hint 0 ≔ S:Alpha, A,B:re (carr (acarr S));
+ SS ≟ carr (acarr S),
+ MM ≟ mk_unary_morphism ?? (λA.
+ mk_unary_morphism ??
+ (λB.A + B) (prop1 ?? (fun1 ?? (o_is_morph S) A)))
+ (prop1 ?? (o_is_morph S)),
+ T ≟ RE S
+(*--------------------------------------------------------------------------*) ⊢
+ fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ o SS A B.
+
+nlemma k_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A).
+#A; @(λs1:re A. s1^* ); #a; nelim a; /2/ by conj; nqed.
+
+unification hint 0 ≔ S:Alpha, A:re (carr (acarr S));
+ SS ≟ carr (acarr S),
+ MM ≟ mk_unary_morphism ?? (λB.B^* ) (prop1 ?? (k_is_morph S)),
+ T ≟ RE S
+(*--------------------------------------------------------------------------*) ⊢
+ fun1 T T MM A ≡ k SS A.
+
+nlemma s_is_morph : ∀A:Alpha.A ⇒_0 (re A).
+#A; @(λs1:A. s ? s1 ); #x y E; //; nqed.
+
+unification hint 0 ≔ S:Alpha, a: carr (acarr S);
+ SS ≟ carr (acarr S),
+ MM ≟ mk_unary_morphism ?? (λb.s ? b ) (prop1 ?? (s_is_morph S)),
+ T ≟ RE S, T1 ≟ acarr S
+(*--------------------------------------------------------------------------*) ⊢
+ fun1 T1 T MM a ≡ s SS a.
+
+(* end setoids support for re *)