proposition: Lemma Equiv_empty : forall m s t,NumMap.Empty m -> Equiv m s t -> s = t.
proof: Proof. intros m s t He [x H H']. inversion_clear H; inversion_clear H'; subst; trivial. firstorder. firstorder. firstorder. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)