proposition: Lemma Forall2_fmap_1 {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. revert k; induction l; intros [|??]; inv 1; auto. Qed.
imports: stdpp(options)