proposition: Lemma NumMap_Equal_Empty_empty : forall elt (t : NumMap.t elt) , NumMap.Empty t -> NumMap.Equal t (NumMap.empty _).
proof: Proof. intros elt t H a. find_analyse; find_tac; firstorder. assert (NumMap.Empty (NumMap.empty elt)). auto with map. firstorder. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)