proposition: Fact subcode_sss_terminates_inv P Q st st1 : Q // st ↓ -> P <sc Q -> P // st ~~> st1 -> Q // st1 ↓.
proof: Proof. Proof using sss_fun. intros (st3 & (k & H1) & H2) H3 ((p & H4) & H5). destruct subcode_sss_subcode_inv with (2 := H3) (3 := H4) (4 := H1) as (q & _ & H6). 1: revert H2; apply subcode_out_code; auto. exists st3; split; auto; exists q; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)