proposition: Fact subcode_snoc_inv i j a l : j = i+length l -> (i,l++a) <sc Q -> (j,a) <sc Q.
proof: Proof. intros H. apply subcode_trans. exists l, nil; split; auto. solve list eq. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)