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