proposition: Lemma eval_inj: forall A B x y z, eval A B x y -> eval A B x z -> y==z.
proof: Proof. intros A B x y z H; revert z; induction H; intros; eval_inversion; trivial. destruct (eval_type_inj_left H0 H4) as [HB | Hx]. destruct HB. rewrite (IHeval1 _ H3), (IHeval2 _ H4); reflexivity. rewrite (eval_clean_zero H0), (eval_clean_zero H4) by (rewrite Hx; reflexivity). rewrite 2 dot_ann_right; reflexivity. rewrite (IHeval1 _ H3), (IHeval2 _ H4); reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)