proposition: Fact subcode_start_in_code : forall P Q, 0 < code_length P -> P <sc Q -> in_code (code_start P) Q.
proof: Proof. intros (iP,cP) (iQ,cQ) H (l & r & H1 & H2); simpl in *; subst; revert H; rew length; intro; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)