proposition: Fact subcode_length' P Q : P <sc Q -> length (snd P) <= length (snd Q).
proof: Proof. revert P Q; intros [] [] (? & ? & ? & ?); simpl; subst; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)