proposition: Fact sss_steps_stop_fun P a b st1 st2 st3 : out_code (fst st2) P -> out_code (fst st3) P -> P // st1 -[a]-> st2 -> P // st1 -[b]-> st3 -> a = b /\ st2 = st3.
proof: Proof. Proof using sss_fun. intros H1 H2 H3 H4. assert (a = b) as Hab. { destruct subcode_sss_subcode_inv with (3 := H3) (4 := H4) as (u & Hu & _); auto. destruct subcode_sss_subcode_inv with (3 := H4) (4 := H3) as (v & Hv & _); auto. lia. } split; auto; subst b. revert H3 H4; apply sss_steps_fun. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)