fact: Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt := match s with | nil => (k,x) :: nil | (k',y) :: l => match X.compare k k' with | LT _ => (k,x)::s | EQ _ => (k,x)::l | GT _ => (k',y) :: add k x l end end.
imports: FMapInterface