proposition: Lemma nth_map : forall `{IA:Inhab A} `{IB:Inhab B} (f:A->B) (l:list A) n, n < length l -> nth n (map f l) = f (nth n l).
proof: Proof. Proof using. introv N. applys nth_of_Nth. applys Nth_map. applys~ Nth_of_nth. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)