proposition: Lemma repr_inj_right : forall a b, repr t a b -> forall c, repr t a c -> b = c.
proof: Proof. induction 1; intros. inversion H0. trivial. find_tac. inversion H1. subst. find_tac. subst. find_tac. eauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)