proposition: Fact in_code_subcode i P : in_code i P -> exists a, (i,a::nil) <sc P.
proof: Proof. destruct P as (iP,cP); simpl; intros H. destruct (list_split_length cP) with (k := i-iP) as (l & [ | a r ] & H1 & H2). + lia. + exfalso; subst; solve list eq in H; lia. + exists a, l, r; split; auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)