proposition: Fact sss_steps_output_fun P a b st1 st2 st3 : P // st1 ~[a]~> st2 -> P // st1 ~[b]~> st3 -> a = b /\ st2 = st3.
proof: Proof. Proof using sss_fun. intros (H1 & H2) (H3 & H4). revert H1 H3; apply sss_steps_stop_fun; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)