proposition: Fact sss_steps_inv P k st1 st3 : P // st1 -[k]-> st3 -> (k = 0 /\ st1 = st3) + { k' | exists st2, k = S k' /\ P // st1 :1> st2 /\ P // st2 -[k']-> st3 }%type.
proof: Proof. intros H. destruct k as [ | k ]; [ left | right ]. apply sss_steps_0_inv in H; auto. exists k. inversion H; subst. exists st2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)