proposition: Lemma list_fmap_ext (f g : A → B) l : (∀ i x, l !! i = Some x → f x = g x) → f <$> l = g <$> l.
proof: Proof. intros Hfg. apply list_eq; intros i. rewrite !list_lookup_fmap. destruct (l !! i) eqn:?; f_equal/=; eauto. Qed.
imports: stdpp(options)