proposition: Fact subcode_app_invert_right j Q1 Q2 i I : (i,I::nil) <sc (j,Q1++Q2) -> (i,I::nil) <sc (j,Q1) \/ (i,I::nil) <sc (length Q1+j,Q2).
proof: Proof. intros (l & r & H1 & H2); simpl in *. apply list_app_cons_eq_inv in H1. destruct H1 as [ (m & G1 & G2) | (m & G1 & G2) ]; subst. + right; exists m, r; rew length; split; auto; lia. + left; exists l, m; rew length; split; auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)