-STOP
- nchange in match (𝐋\p (pk ? e')) with (𝐋\p e' · 𝐋 |e'|^* );
- nrewrite > (erase_bull…e);
- nrewrite > (erase_star …);
- nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 .|e| - ϵ b')); ##[##2:
- 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…);
- nrewrite > (?: ((?·?)∪{[]} = 𝐋 .|e^*|)); //;
- nchange in match (𝐋 .|e^*|) with ((𝐋. |e|)^* ); napply sub_dot_star;##]
+ (* nwhd in match (𝐋\p e'^* ); (* XXX bug uncertain *) *)
+ nchange in ⊢ (???(??%?)?) with (𝐋\p e' · ?);
+ napply (.=_1 (# ╪_1 (┼_1 (┼_0 (erase_bull S e)))) ╪_1 #);
+ napply (.=_1 (# ╪_1 (erase_star …)) ╪_1 #);
+ ncut ( 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[
+ nchange in IH : (???%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH;
+ ##[ #IH; napply (?^-1); napply (.=_1 (cup_sub … (not_epsilon_lp…)));
+ napply (.=_1 (IH^-1 ╪_1 #));
+ alias symbol "invert" = "setoid1 symmetry".
+ (* XXX too slow if ambiguous, since it tries with a ? (takes 12s) then
+ tries with sym0 and fails immediately, then with sym1 that is OK *)
+ napply (.=_1 (cup_sub …(not_epsilon_lp …))^-1);
+ napply (.=_1 # ╪_1 (subK…)); napply (.=_1 (cup0…)); //;
+ ##| #IH; napply (?^-1); napply (.=_1 # ╪_1 (sub0 …));
+ napply (.=_1 IH^-1); napply (.=_1 (cup0 …)); //; ##]##] #EE;
+ napply (.=_1 (EE ╪_1 #) ╪_1 #);
+ napply (.=_1 (cup_dotD…) ╪_1 #);
+ napply (.=_1 (cupA…));
+ napply (.=_1 # ╪_1 (sub_dot_star…)); //; ##]