proposition: Fact subcode_length P Q : P <sc Q -> code_start Q <= code_start P /\ code_end P <= code_end Q.
proof: Proof. destruct P as (iP,cP); destruct Q as (iQ,cQ); simpl. intros (l & r & H1 & H2). apply f_equal with (f := @length _) in H1. revert H1; rew length; split; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)