proposition: Lemma vec_pos_gt n X (w : vec X n) j k n1: pos2nat k < pos2nat j -> vec_pos w j = vec_pos (vec_change w k n1) j.
proof: Proof. intros. induction w. - invert pos j. - invert pos j; cbn. + invert pos k; cbn; auto; lia. + invert pos k; cbn; auto. apply IHw. rewrite !pos2nat_nxt in H; lia. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract