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