proposition: Fact vec_pos_set n (g : pos n -> X) p : vec_pos (vec_set_pos g) p = g p.
proof: Proof. revert g p; induction n as [ | n IHn ]; intros g p; pos_inv p; auto. apply IHn. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)