proposition: Fact subcode_sss_compute_instr P i st1 st2 st3 : i // st1 -1> st2 -> (fst st1,i::nil) <sc P -> P // st2 ->> st3 -> P // st1 ->> st3.
proof: Proof. intro H; apply subcode_sss_compute_linstr with (k := 1). apply sss_steps_1, in_sss_step with (l := nil); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)