proposition: Fact sss_output_fun P st st1 st2 : P // st ~~> st1 -> P // st ~~> st2 -> st1 = st2.
proof: Proof. Proof using sss_fun. intros (H1 & H2) (H3 & H4); revert H2 H4 H1 H3; apply sss_compute_fun. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)