proposition: Lemma sameclass_empty : forall s t, sameclass empty s t -> s = t.
proof: Proof. intros. refine (Equiv_empty _ _ _ _ H). simpl. apply NumMap.empty_1. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)