proposition: Lemma repr_zero_inv : forall i x, i <> x -> ~NumMap.In i t -> ~ repr t i x.
proof: Proof. intros i x Hix H. intro H'; inversion H'. subst. tauto_false. subst. apply H. eexists. eassumption. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)