proposition: Fact subcode_sss_steps P Q k st1 st2: P <sc Q -> P // st1 -[k]-> st2 -> Q // st1 -[k]-> st2.
proof: Proof. induction 2 as [ | k st1 st2 st3 H3 H4 IH4 ]. constructor. constructor 2 with st2; auto. revert H3; apply subcode_sss_step; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)