proposition: Lemma index_map_eq : forall A B (l:list A) i (f:A->B), index (map f l) i = index l i.
proof: Proof. Proof using. intros. rewrite index_eq_inbound in *. rewrite~ length_map. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)