proposition: Lemma get_dec : forall x E, { v : A | get x E = Some v } + { get x E = None }.
proof: Proof. intros. induction E as [ | (y, w) ]. right; auto. simpl. destruct (eq_keys_dec x y). left; exists w; auto. auto. Qed.
imports: Utf8 Equalities