proposition: Fact subcode_cons P n x l : P <sc (1+n,l) -> P <sc (n,x::l).
proof: Proof. intros; apply subcode_trans with (1 := H). exists (x::nil), nil; split. solve list eq. rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)