proposition: Fact subcode_sss_progress_inv P Q p st1 st2 st3 : out_code (fst st3) P -> P <sc Q -> P // st1 -+> st2 -> Q // st1 -[p]-> st3 -> exists q, q < p /\ Q // st2 -[q]-> st3.
proof: Proof. Proof using sss_fun. intros H1 H2 (k & ? & H3) H4. apply subcode_sss_subcode_inv with (3 := H3) in H4; auto. destruct H4 as (q & ? & ?); exists q; split; auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)