nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH;
##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH;
nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//;
##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##]
nrewrite > (cup_dotD…); nrewrite > (cupA…);
nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH;
##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH;
nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//;
##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##]
nrewrite > (cup_dotD…); nrewrite > (cupA…);