proposition: Fact sss_steps_stall_fun P p q s1 s2 : sss_step_stall P s2 -> P // s1 -[p]-> s2 -> P // s1 -[q]-> s2 -> p = q.
proof: Proof. Proof using sss_fun. intros H1 H2; revert H2 q. induction 1 as [ s1 | p s1 s2 s3 H2 H3 IH3 ]; intros q H5. apply sss_steps_stall_inv, proj1 in H5; auto. destruct q. apply sss_steps_0_inv in H5; subst. apply H1 in H2; destruct H2. specialize (IH3 H1). apply sss_steps_S_inv' in H5. destruct H5 as (st2' & H5 & H6). generalize (sss_step_fun H2 H5). intros; subst st2'. apply IH3 in H6; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)