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