fact: Fixpoint eq_list (m m' : list (key * elt)) : Prop := match m, m' with | nil, nil => True | (x,e)::l, (x',e')::l' => match compare x x' with | EQ _ => eq e e' /\ eq_list l l' | _ => False end | _, _ => False end.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses