proposition: Fact sss_steps_fun P k s t1 t2 : P // s -[k]-> t1 -> P // s -[k]-> t2 -> t1 = t2.
proof: Proof. Proof using sss_fun. intros H; revert H t2; induction 1 as [ | ? ? st2 ? H1 H2 IH2 ]; simpl; intros t2 Ht2; auto. inversion Ht2; auto. inversion Ht2; subst. generalize (sss_step_fun H1 H0); intro; subst. apply IH2 in H3; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)