proposition: Lemma list_omap_ext {A'} (g : A' → option B) l1 (l2 : list A') : Forall2 (λ a b, f a = g b) l1 l2 → omap f l1 = omap g l2.
proof: Proof. induction 1 as [|x y l l' Hfg ? IH]; [done|]. csimpl. rewrite Hfg. destruct (g y); [|done]. by f_equal. Qed.
imports: stdpp(options)