proposition: Fact subcode_cons_invert_left i I l : (i,I::l) <sc Q -> (i,I::nil) <sc Q /\ (S i,l) <sc Q.
proof: Proof. intros H1; split. + revert H1; apply subcode_cons_inv with (a := _::nil); auto. + revert H1; apply subcode_snoc_inv with (l := _::nil); simpl; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils)