proposition: Lemma ALFindSome : forall sub : AssocList, forall v : Key, forall u : Value, ALFind sub v = Some u -> LIn (v, u) sub.
proof: Proof. induction sub; simpl; sp. inversion H. destruct (DeqKey v a0); cpx. Qed.
imports: list Omega