proposition: Fact subcode_sss_terminates P Q st : P <sc Q -> Q // st ↓ -> P // st ↓.
proof: Proof. intros H (st' & H1 & H2). apply subcode_sss_compute_inv with (1 := H) in H1; auto. + destruct H1 as (st2 & H1 & H3 & H4). exists st2; split; auto. + revert H2; apply subcode_out_code; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(Utils.utils Code.subcode)