lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! [] = refl
lem-tab-! (x :: xs) = {!!}


Goal: (x :: tabulate ((λ {.x} → _!_ (x :: xs)) ◦ fsucc)) ==
      (x :: xs)
————————————————————————————————————————————————————————————
xs : Vec .A .n
x  : .A
.A : Set
.n : Nat