+(* hints for epsilon *)
+nlemma epsilon_is_morph : βA:Alpha. (setoid1_of_setoid bool) β_1 (lang A).
+#X; @; ##[#b; napply(Ο΅ b)] #a1 a2; ncases a1; ncases a2; //; *; nqed.
+
+nlemma epsilon_is_ext: βA:Alpha. (setoid1_of_setoid bool) β (Elang A).
+ #S b; @(Ο΅ b); #w1 w2 E; ncases b; @; ##[##3,4:*]
+nchange in match (w1 β Ο΅ true) with ([] =_0 w1);
+nchange in match (w2 β Ο΅ true) with ([] =_0 w2); #H; napply (.= H); /2/;
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 β A : Alpha, B : bool;
+ AA β LIST (acarr A),
+ R β mk_ext_powerclass ?
+ (Ο΅ B) (ext_prop ? (epsilon_is_ext ? B))
+(*--------------------------------------------------------------------*) β’
+ ext_carr AA R β‘ epsilon A B.
+
+unification hint 0 β S:Alpha, A:bool;
+ B β setoid1_of_setoid BOOL,
+ T β powerclass_setoid (list (carr (acarr S))),
+ MM β mk_unary_morphism1 B T
+ (Ξ»B.Ο΅ B) (prop11 B T (epsilon_is_morph S))
+(*--------------------------------------------------------------------------*) β’
+ fun11 B T MM A β‘ epsilon S A.
+
+nlemma epsilon_is_ext_morph:βA:Alpha. (setoid1_of_setoid bool) β_1 (Elang A).
+#A; @(epsilon_is_ext β¦);
+#x1 x2 Ex; napply (prop11 β¦ (epsilon_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 β AA : Alpha, B : bool;
+ AAS β LIST (acarr AA),
+ BB β setoid1_of_setoid BOOL,
+ T β ext_powerclass_setoid AAS,
+ R β mk_unary_morphism1 BB T
+ (Ξ»S.
+ mk_ext_powerclass AAS (epsilon AA S)
+ (ext_prop AAS (epsilon_is_ext AA S)))
+ (prop11 BB T (epsilon_is_ext_morph AA))
+(*------------------------------------------------------*) β’
+ ext_carr AAS (fun11 BB T R B) β‘ epsilon AA B.
+
+(* end hints for epsilon *)
+