fact: Fixpoint tabulate {X : Type} (n : nat) (f : Fin.t n -> X) {struct n} : Vector.t X n := match n as m return ((Fin.t m -> X) -> t X m) with | 0 => fun _ => [] | S m => fun f => f Fin.F1 :: @tabulate _ m (fun i => f (Fin.FS i)) end f.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List