-nlemma cup_sub: ∀S:Alpha.∀a,b:Elang S. ¬ ([]∈ a) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
-#S a b c; napply ext_set; #w; @;
-##[ *; ##[ #wa; @; ##[@;//] #H; napply c; napply (. ?╪_0?);
- napply (. (memnil ?? H)^-1‡#);
-/4/; *; /4/; nqed.
+nlemma cup_sub: ∀S.∀A,B:𝛀^S.∀x. ¬ (x ∈ A) → A ∪ (B - {(x)}) = (A ∪ B) - {(x)}.
+#S A B x H; napply ext_set; #w; @;
+##[ *; ##[ #wa; @; ##[@;//] #H2; napply H; napply (. (mem_single ??? H2)^-1╪_1#); //]
+ *; #wb nwn; @; ##[@2;//] //;
+##| *; *; ##[ #wa nwn; @; //] #wb nwn; @2; @; //;##]
+nqed.