proposition: Fact subcode_trans P Q R : P <sc Q -> Q <sc R -> P <sc R.
proof: Proof. revert P Q R; intros (iP,cP) (iQ,cQ) (iR,cR). intros (ll1 & rr1 & H1 & H2) (ll2 & rr2 & H3 & H4); subst. exists (ll2++ll1), (rr1++rr2); split. solve list eq. rew length; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)