proposition: Fact vec_list_iso n v : list_vec (@vec_list n v) = eq_rect_r _ v (vec_list_length v).
proof: Proof. induction v; simpl; f_equal; auto. rewrite IHv; unfold eq_rect_r; simpl. generalize (length (vec_list v)) (vec_list_length v). intros; subst; cbv; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)