proposition: Lemma eq_nat_spec : forall n m, n = m <-> nat_of_num n = nat_of_num m.
proof: Proof. intuition subst. reflexivity. setoid_rewrite <- id_num. rewrite H. reflexivity. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)