proposition: Lemma Nth_map : forall (A B:Type) (f:A->B) (l:list A) n (x:A), Nth n l x -> Nth n (map f l) (f x).
proof: Proof. Proof using. #[global] Hint Constructors Nth. introv M. induction M; rew_listx; auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)