proposition: Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) : list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
proof: Proof. induction l as [|x l IH]; [done|]; csimpl. case_decide; [done|]. rewrite IH. by destruct (list_find (P ∘ f) l). Qed.
imports: stdpp(options)