+(* support for 𝐋 as an extensional set *)
+ndefinition L_re_is_ext : ∀S:Alpha.∀r:re S.Elang S.
+#S r; @(𝐋 r); #w1 w2 E; nelim r;
+##[ ##1,2: /2/; @; #defw1; napply (.=_0 (defw1 : [ ] = ?)); //; napply (?^-1); //;
+##| #x; @; #defw1; napply (.=_0 (defw1 : [x] = ?)); //; napply (?^-1); //;
+##| #e1 e2 H1 H2; (* not shure I shoud Inline *)
+ @; *; #s1; *; #s2; *; *; #defw1 s1L1 s2L2;
+ ##[ nlapply (trans … E^-1 defw1); #defw2;
+ ##| nlapply (trans … E defw1); #defw2; ##] @s1; @s2; /3/;
+##| #e1 e2 H1 H2; napply (H1‡H2); (* good! *)
+##| #e H; @; *; #l; *; #defw1 Pl; @l; @; //; napply (.=_1 defw1); /2/; ##]
+nqed.
+
+unification hint 0 ≔ S : Alpha,e : re (carr (acarr S));
+ SS ≟ LIST (acarr S),
+ X ≟ mk_ext_powerclass SS (𝐋 e) (ext_prop SS (L_re_is_ext S e))
+(*-----------------------------------------------------------------*)⊢
+ ext_carr SS X ≡ L_re S e.
+
+nlemma L_re_is_morph:∀A:Alpha.(setoid1_of_setoid (re A)) ⇒_1 Ω^(list A).
+#A; @; ##[ napply (λr:re A.𝐋 r); ##] #r1; nelim r1;
+##[##1,2: #r2; ncases r2; //; ##[##1,6: *|##2,7,5,12,10: #a; *|##3,4,8,9: #a1 a2; *]
+##|#x r2; ncases r2; ##[##1,2: *|##4,5: #a1 a2; *|##6: #a; *] #y E; @; #z defz;
+ ncases z in defz; ##[##1,3: *] #zh ztl; ncases ztl; ##[##2,4: #d dl; *; #_; *]
+ *; #defx; #_; @; //; napply (?^-1); napply (.= defx^-1); //; napply (?^-1); //;
+##|#e1 e2 IH1 IH2 r2; ncases r2; ##[##1,2: *|##5: #a1 a2; *|##3,6: #a1; *]
+ #f1 f2; *; #E1 E2; nlapply (IH2 … E2); nlapply (IH1 … E1); #H1 H2;
+ nchange in match (𝐋 (e1 · e2)) with (?·?);
+ napply (.=_1 (H1 ╪_1 H2)); //;
+##|#e1 e2 IH1 IH2 r2; ncases r2; ##[##1,2: *|##4: #a1 a2; *|##3,6: #a1; *]
+ #f1 f2; *; #E1 E2; nlapply (IH2 … E2); nlapply (IH1 … E1); #H1 H2;
+ napply (.=_1 H1╪_1H2); //;
+##|#r IH r2; ncases r2; ##[##1,2: *|##4,5: #a1 a2; *|##3: #a1; *]
+ #e; #defe; nlapply (IH e defe); #H;
+ @; #x; *; #wl; *; #defx Px; @wl; @; //; nelim wl in Px; //; #l ls IH; *; #lr Pr;
+ ##[ nlapply (ifs' … H … lr) | nlapply (ifs' … H^-1 … lr) ] #le;
+ @; ##[##1,3: nassumption] /2/; ##]
+nqed.
+
+unification hint 0 ≔ A:Alpha, a:re (carr (acarr A));
+ T ≟ setoid1_of_setoid (RE A),
+ T2 ≟ powerclass_setoid (list (carr (acarr A))),
+ MM ≟ mk_unary_morphism1 ??
+ (λa:carr1 (setoid1_of_setoid (RE A)).𝐋 a) (prop11 ?? (L_re_is_morph A))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 T T2 MM a ≡ L_re A a.
+
+nlemma L_re_is_ext_morph:∀A:Alpha.(setoid1_of_setoid (re A)) ⇒_1 𝛀^(list A).
+#A; @; ##[ #a; napply (L_re_is_ext ? a); ##] #a b E;
+ncut (𝐋 b = 𝐋 a); ##[ napply (.=_1 (┼_1 E^-1)); // ] #EL;
+@; #x H; nchange in H ⊢ % with (x ∈ 𝐋 ?);
+##[ napply (. (# ╪_1 ?)); ##[##3: napply H |##2: ##skip ] napply EL;
+##| napply (. (# ╪_1 ?)); ##[##3: napply H |##2: ##skip ] napply (EL^-1)]
+nqed.
+
+unification hint 1 ≔ AA : Alpha, a: re (carr (acarr AA));
+ T ≟ RE AA, T1 ≟ LIST (acarr AA), T2 ≟ setoid1_of_setoid T,
+ TT ≟ ext_powerclass_setoid T1,
+ R ≟ mk_unary_morphism1 T2 TT
+ (λa:carr1 (setoid1_of_setoid T).
+ mk_ext_powerclass T1 (𝐋 a) (ext_prop T1 (L_re_is_ext AA a)))
+ (prop11 T2 TT (L_re_is_ext_morph AA))
+(*------------------------------------------------------*) ⊢
+ ext_carr T1 (fun11 (setoid1_of_setoid T) TT R a) ≡ L_re AA a.
+
+(* end support for 𝐋 as an extensional set *)