-ninductive eq2 (A : Type[1]) (a : A) : A â CProp[0] â
-| refl2 : eq2 A a a.
-
-interpretation "eq2" 'eq T a b = (eq2 T a b).
-
-ntheorem th_ch3: ÂŹâa:caxs.âx.Ď a x = h x.
-*; #a; #H;
-ncut ((đ a one) â { x | x â â
}); (* bug *)
-nchange in xx with { x | h x
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-ntheorem cantor: âa:axs. ÂŹ (Z â R a ⧠R a â Z).
-#a; *; #ZRa; #RaZ;
-ncut (a â R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
-ncut (a â â
); ##[
- napply (cover_trans ⌠H1);
- #x; #H; nlapply (RaZ ⌠H); #ABS; napply ABS; ##] #H2;
-ncut (a â R a); ##[ napply ZRa; napply H2; ##] #H3;
-nelim H2 in H3;
-##[ nauto.
-##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
-nqed.
-
-ninductive deduct (A : nAx) (U : Ί^A) : A â CProp[0] â
-| drefl : âa.a â U â deduct A U a
-| dcut : âa.âi:đ a. (ây:đ a i.deduct A U (đ a i y)) â deduct A U a.
-
-notation " a ⢠b " non associative with precedence 45 for @{ 'deduct $a $b }.
-interpretation "deduct" 'deduct a b = (deduct ? b a).
-
-ntheorem th2_3_1 : âA:nAx.âa:A.âi:đ a. a ⢠đđŚ[đ a i].
-#A; #a; #i;
-ncut (ây:đ a i.đ a i y ⢠đđŚ[đ a i]); ##[ #y; @; @y; @; ##] #H1;
-napply (dcut ⌠i); nassumption;
+nlemma replace_char:
+ âA:Ax.âU,V.U â V â V â U â âa:A.a â U â a â V.
+#A; #U; #V; #UV; #VU; #a; #aU; nelim aU; //;