- nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
- nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
- nrewrite > (IH1 …); nrewrite > (cup_dotD …);
- nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
- nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
- nrewrite < (erase_dot …); nrewrite < (cupA …); //;
+ nchange in match (•(e1·e2)) with (•e1 ⊙ 〈e2,false〉);
+ napply (.=_1 (odot_dot_aux ?? 〈e2,false〉 IH2));
+ napply (.=_1 (IH1 ╪_1 #) ╪_1 #);
+ napply (.=_1 (cup_dotD …) ╪_1 #);
+ napply (.=_1 (cupA …));
+ napply (.=_1 # ╪_1 ((erase_dot ???)^-1 ╪_1 (cup0 ??)));
+ napply (.=_1 # ╪_1 (cupC…));
+ napply (.=_1 (cupA …)^-1);
+ //;