proposition: Fact subcode_sss_steps_inv_1 P i k st1 st2 st3 : st1 <> st3 -> i // st1 -1> st2 -> (fst st1,i::nil) <sc P -> P // st1 -[k]-> st3 -> exists k', k = S k' /\ P // st2 -[k']-> st3.
proof: Proof. Proof using sss_fun. intros H1 H2 H3 H4. apply sss_steps_inv in H4. destruct H4 as [ (_ & H4) | (k' & st & ? & H4 & ?) ]. contradict H1; auto. exists k'; split; auto. apply subcode_sss_step_inv_1 with (1 := H3) in H4. rewrite (sss_fun H2 H4); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)