proposition: Lemma ALFind2 : forall (sub: AssocList) (a : Key) , { b: Value & LIn (a,b) sub} + !(LIn a (ALDom sub)).
proof: Proof. induction sub as [| (a', b') sub Hind]; intro a. - right. sp. - destruct (DeqKey a a') as [Hc|Hc]; subst. + left. exists b'. left; refl. + destruct (Hind a) as [Hl | Hr]; exrepnd ;[left | right]. * exists b. right; auto. * intro Hf. apply Hr. simpl in Hf. destruct (split sub). dorn Hf; sp. Defined.
imports: list Omega