proposition: Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l : (∀ x, P x ↔ Q x) → list_find P l = list_find Q l.
proof: Proof. intros HPQ. induction l as [|x l IH]; simpl; [done|]. by rewrite (decide_ext (P x) (Q x)), IH by done. Qed.
imports: stdpp(options)