proposition: Lemma list_fmap_equiv_ext `{!Equiv B} (f g : A → B) l : (∀ i x, l !! i = Some x → f x ≡ g x) → f <$> l ≡ g <$> l.
proof: Proof. intros Hl. apply list_equiv_lookup; intros i. rewrite !list_lookup_fmap. destruct (l !! i) eqn:?; simpl; constructor; eauto. Qed.
imports: stdpp(options)