proposition: Fact subcode_out_code P Q i : P <sc Q -> out_code i Q -> out_code i P.
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)