proposition: Fact mm_sss_total ii s : { t | ii // s -1> t }.
proof: Proof. destruct s as (i,v). destruct ii as [ x | x j ]; [ | case_eq (v#>x); [ | intros k ]; intros E ]. * exists (1+i,v[(S (v#>x))/x]); constructor. * exists (j,v); constructor; auto. * exists (1+i,v[k/x]); constructor; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)