proposition: Fact mma_sss_INC_inv x i v j w : INCₐ x // (i,v) -1> (j,w) -> j=1+i /\ w = v[(S (v#>x))/x].
proof: Proof. inversion 1; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)