fact: Fixpoint Vector_pow {X: Type} (A: list X) n {struct n} : list (Vector.t X n) := match n with | 0 => [Vector.nil _] | S n => concat (map (fun a => map (fun v => a:::v) (Vector_pow A n) ) A) end.
imports: Undecidability.Shared.Libs.PSL(BasicDefinitions) Undecidability.Shared.Libs.PSL(FiniteTypes.FinTypes) Undecidability.Shared.Libs.PSL(Vectors.Vectors)