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