proposition: Fact subcode_length_le : forall P Q, P <sc Q -> fst Q <= fst P /\ fst P + length (snd P) <= fst Q + length (snd Q).
proof: Proof. intros (iP,cP) (iQ,cQ) (l & r & ? & ?); subst; simpl; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)