proposition: Corollary mma_sss_compute_INC P i x v st : (i,INCₐ x::nil) <sc P -> P // (1+i,v[(S (v#>x))/x]) ->> st -> P // (i,v) ->> st.
proof: Proof. intros; apply sss_progress_compute; eapply mma_sss_progress_INC; eauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)