fact: Fixpoint eq_list (m m' : list (X.t * D.t)) : Prop := match m, m' with | nil, nil => True | (x,e)::l, (x',e')::l' => match X.compare x x' with | EQ _ => D.eq e e' /\ eq_list l l' | _ => False end | _, _ => False end.
imports: FMapInterface