proposition: Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l k : Forall2 P (f <$> l) (g <$> k) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l k.
proof: Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
imports: stdpp(options)