proposition: Fact sss_step_fun P s t1 t2 : P // s :1> t1 -> P // s :1> t2 -> t1 = t2.
proof: Proof. Proof using sss_fun. intros (k1 & l1 & i1 & r1 & d1 & ? & ? & H1) (k2 & l2 & i2 & r2 & d2 & ? & ? & H2). subst. inversion H3. inversion H4. subst k2. apply list_app_inj in H5; try lia. destruct H5 as (? & H5); inversion H5. subst. revert H1 H2; apply sss_fun. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)