proposition: Lemma ALKeepFirstLin: forall sub v vs t, LIn (v,t) (ALKeepFirst sub vs) <=> (ALFind sub v = Some t # LIn v vs).
proof: Proof. induction sub; simpl; sp;[split;sp|]. destruct (DeqKey v a0); destruct (in_deq Key DeqKey a0 vs); subst; cpx; split; introns Hyp; allsimpl; exrepnd; cpx. - dorn Hyp; cpx. apply IHsub in Hyp. exrepnd. apply in_remove in Hyp; cpx. - apply IHsub in Hyp; exrepnd; cpx. - dorn Hyp; cpx. apply IHsub in Hyp. exrepnd. apply in_remove in Hyp; cpx. - right. apply IHsub; dands; cpx. apply in_remove; dands; cpx. Qed.
imports: list Omega