proposition: Lemma Forall_fmap_ext (g : A → B) (l : list A) : Forall (λ x, f x = g x) l ↔ fmap f l = fmap g l.
proof: Proof. split; [auto using Forall_fmap_ext_1|]. induction l; simpl; constructor; simplify_eq; auto. Qed.
imports: stdpp(options)