proposition: Theorem mm_special_ind s : P // s ->> se -> Q s.
proof: Proof. Proof using HQ0 HQ1. intros (q & H1); revert s H1. induction q as [ | q IHq ]; intros s Hs. + apply sss_steps_0_inv in Hs; subst; apply HQ0. + apply sss_steps_S_inv' in Hs. destruct Hs as ((j,w) & (j' & l & ρ & r & u & G1 & G2 & G3) & Hs2); subst s P. apply HQ1 with (i := j'+length l) (2 := G3); auto. exists q; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)