proposition: Lemma Nth_map_inv : forall (A B:Type) (f:A->B) (l:list A) n (y:B), Nth n (map f l) y -> exists x, y = f x /\ Nth n l x.
proof: Proof. Proof using. introv N. gen n. induction l; introv N. { inverts N. } { rewrite map_cons in N. inverts N as N. { autos*. } { lets (x&E&N'): IHl N. exists* x. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)