proposition: Lemma eqb_true : forall x y, eqb x y = true <-> x = y.
proof: Proof. intros. case eq_spec; intuition discriminate. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)