proposition: Lemma find_Some `{finA: Finite A} (P : A → Prop) `{∀ x, Decision (P x)} (x : A) : find P = Some x → P x.
proof: Proof. destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl. intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=. rewrite !Nat2Pos.id in Hx by done. destruct (list_find_Some P xs i y); naive_solver. Qed.
imports: stdpp(options)