proposition: Lemma Forall2_map_r : forall f P l, (forall x, P x (f x)) -> Forall2 P l (map f l).
proof: Proof. Proof using. introv I. induction l; rew_listx~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)