proposition: Lemma ALFindSomeKeepFirstSingleton: forall sub v t, ALFind sub v = Some t -> ALKeepFirst sub [v] = [(v,t)].
proof: Proof. induction sub as [|(v,t) sub Hind]; introv Heq; allsimpl; cpx. destruct (DeqKey v0 v) as [xx|xx]; subst;allsimpl; cpx;[]. rewrite DeqTrue. rw ALKeepFirstNil; auto. Qed.
imports: list Omega