proposition: Lemma list_map_nth : forall A (f : A -> A) (d : A) (l : list A) (n : nat), f d = d -> f (List.nth n l d) = List.nth n (LibList.map f l) d.
proof: Proof. Proof using. induction l; introv E; destruct n; rew_listx; simpl; auto. Qed.
imports: TLC(LibList)