proposition: Lemma NumMap_fold_compat A t f g (x: A): (forall acc (k e : num) , f k e acc = g k e acc) -> NumMap.fold f t x = NumMap.fold g t x.
proof: Proof. intros. setoid_rewrite NumMap.fold_1. revert x. induction (NumMap.elements t); simpl; intros. reflexivity. rewrite H. apply IHl. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)