proposition: Lemma find_opt_spec {A} (l : list A) (f : A -> option A) : match find_opt l f with | Some x => exists a, In a l /\ f a = Some x | None => forall a, In a l -> f a = None end.
proof: Proof. funelim (find_opt l f); intros. elim H. exists x; simpl; intuition eauto. destruct (find_opt xs f); now firstorder subst. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect