head-eq : {A : Set} {n : Nat} {xs : Vec A n} {ys : Vec A n} -> (x : A) -> xs == ys -> (x :: xs) == (x :: ys)
head-eq {xs = []} {ys = []} x p = refl
head-eq {xs = xs} {ys = ys} x p = refl
-- Error!                         ^^^^
xs != ys of type Vec .A .n
when checking that the expression refl has type
(x :: xs) == (x :: ys)

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






head-eq' : {A : Set} {n : Nat} {xs : Vec A n} -> (x : A) -> xs == xs -> (x :: xs) == (x :: xs)
head-eq' x p = refl

lem-tab-!' : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-!' [] = refl
lem-tab-!' {n = succ n} (x :: xs) = head-eq' x (lem-tab-!' {n = n} xs)
-- Error!                                      ^^^^^
xs != tabulate (_!_ xs) of type Vec .A n
when checking that the expression lem-tab-!' {n = n} xs has type
tabulate (_!_ xs) == tabulate (_!_ xs)