proposition: Lemma read_map : forall `{IA:Inhab A} `{IB:Inhab B} (l:list A) (i:int) (f:A->B), index l i -> (map f l)[i] = f (l[i]).
proof: Proof. Proof using. introv H. rewrite index_eq_inbound in H. unfold read_inst, read_impl. simpl. case_if. { false; math. } { rewrite nth_map. auto. applys lt_nat_of_lt_int. rewrite abs_nonneg; math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)