fact: Fixpoint vec_set_pos n : (pos n -> X) -> vec n := match n return (pos n -> X) -> vec n with | 0 => fun _ => vec_nil | S n => fun g => g pos0 ## vec_set_pos (fun p => g (pos_nxt p)) end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)