+(* hints for cat *)
+nlemma cat_is_morph : ∀A:setoid. (lang A) ⇒_1 (lang A) ⇒_1 (lang A).
+#X; napply (mk_binary_morphism1 … (λA,B:lang X.A · B));
+#A1 A2 B1 B2 EA EB; napply ext_set; #x;
+ncut (∀y,x:list X.(x ∈ B1) =_1 (x ∈ B2)); ##[
+ #_; #y; ncases EA; ncases EB; #h1 h2 h3 h4; @; ##[ napply h1 | napply h2] ##] #YY;
+ncut (∀x,y:list X.(x ∈ A1) =_1 (x ∈ A2)); ##[
+ #y; #y; ncases EA; ncases EB; #h1 h2 h3 h4; @; ##[ napply h3 | napply h4] ##] #XX;
+napply (.=_1 (∑w1, w2. XX w1 w2/ E ; (# ╪_1 E) ╪_1 #));
+napply (.=_1 (∑w1, w2. YY w1 w2/ E ; # ╪_1 E)); //;
+nqed.
+
+nlemma cat_is_ext: ∀A:setoid. (Elang A) → (Elang A) → (Elang A).
+ #S A B; @ (ext_carr … A · ext_carr … B); (* XXX coercion ext_carr che non funge *)
+#x y Exy;
+ncut (∀w1,w2.(x == w1@w2) = (y == w1@w2)); ##[
+ #w1 w2; @; #H; ##[ napply (.= Exy^-1) | napply (.= Exy)] // ]
+#E; @; #H;
+##[ napply (. (∑w1,w2. (E w1 w2)^-1 / E ; (E ╪_1 #) ╪_1 #)); napply H;
+##| napply (. (∑w1,w2. E w1 w2 / E ; (E ╪_1 #) ╪_1 #)); napply H ]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ A : setoid, B,C : Elang A;
+ AA ≟ LIST A,
+ BB ≟ ext_carr AA B,
+ CC ≟ ext_carr AA C,
+ R ≟ mk_ext_powerclass AA
+ (cat A (ext_carr AA B) (ext_carr AA C))
+ (ext_prop AA (cat_is_ext A B C))
+(*----------------------------------------------------------*) ⊢
+ ext_carr AA R ≡ cat A BB CC.
+
+unification hint 0 ≔ S:setoid, A,B:lang (carr S);
+ T ≟ powerclass_setoid (list (carr S)),
+ MM ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
+ (λA:lang (carr S).
+ mk_unary_morphism1 T T
+ (λB:lang (carr S).cat S A B)
+ (prop11 T T (fun11 ?? (cat_is_morph S) A)))
+ (prop11 T (unary_morphism1_setoid1 T T) (cat_is_morph S))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ cat S A B.
+
+nlemma cat_is_ext_morph:∀A:setoid.(Elang A) ⇒_1 (Elang A) ⇒_1 (Elang A).
+#A; napply (mk_binary_morphism1 … (cat_is_ext …));
+#x1 x2 y1 y2 Ex Ey; napply (prop11 … (cat_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 ≔ AA : setoid, B,C : Elang AA;
+ AAS ≟ LIST AA,
+ T ≟ ext_powerclass_setoid AAS,
+ R ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T) (λX:Elang AA.
+ mk_unary_morphism1 T T (λY:Elang AA.
+ mk_ext_powerclass AAS
+ (cat AA (ext_carr ? X) (ext_carr ? Y))
+ (ext_prop AAS (cat_is_ext AA X Y)))
+ (prop11 T T (fun11 ?? (cat_is_ext_morph AA) X)))
+ (prop11 T (unary_morphism1_setoid1 T T) (cat_is_ext_morph AA)),
+ BB ≟ ext_carr ? B,
+ CC ≟ ext_carr ? C
+(*------------------------------------------------------*) ⊢
+ ext_carr AAS (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ cat AA BB CC.
+
+(* end hints for cat *)
+
+ndefinition star : ∀A:setoid.∀l:lang A.lang A ≝
+ λS.λl.{ w ∈ list S | ∃lw.flatten ? lw = w ∧ conjunct ? lw l}.