proposition: Lemma ALFindDef2Same : forall (key : Key) (def: Value) (al : AssocList), ALFindDef al key def=ALFindDef2 al key def.
proof: Proof. induction al as [|h th Hind]; auto;[]. destruct h as [k v]. allunfold ALFindDef. allunfold ALFindDef2. simpl. cases_ifd Hd; auto. - rw Hdt; auto. - unfold ALFindDef2 in Hind. rw Hind. destruct_head_match; simpl; auto. destruct s; auto. Qed.
imports: list Omega