proposition: Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x : (∃ H : i < n, v !!! nat_to_fin H = x) ↔ (v : list A) !! i = Some x.
proof: Proof. split. - intros [Hlt ?]. rewrite <-(fin_to_nat_to_fin i n Hlt). by apply vlookup_lookup. - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix). rewrite vec_to_list_length in Hlt. exists Hlt. apply vlookup_lookup. by rewrite fin_to_nat_to_fin. Qed.
imports: stdpp(countable) stdpp(options)