idx : (n : Nat) -> (l : List a) -> {auto ok : n < length l = True} -> a
idx Z     (x::xs) {ok=p}    = x
idx (S n) (x::xs) {ok=p}    = idx n xs {ok=rewrite p in Refl}
idx _     []      {ok=Refl} impossible --   = ?foo