proposition: Fact subcode_in_code P Q i : P <sc Q -> in_code i P -> in_code i Q.
proof: Proof. revert P Q; intros (iP,cP) (iQ,cQ) (l & r & H1 & H2); simpl. subst; rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)