proposition: Fact mma_sss_DEC1_inv x k u i v j w : v#>x = S u -> DECₐ x k // (i,v) -1> (j,w) -> j=k /\ w = v[u/x].
proof: Proof. intros H; inversion 1; subst; auto; rewrite H in H2; try discriminate. inversion H2; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)