proposition: Lemma eval_type_inj_left: forall A A' B x z z', eval A B x z -> eval A' B x z' -> A=A' \/ clean0 x = U.zero.
proof: Proof. intros A A' B x z z' H; revert A' z'; induction H; intros A' z' H'; eval_inversion; intuition. destruct (IHeval2 _ _ H3) as [HB | Hy]. destruct HB. destruct (IHeval1 _ _ H2) as [HA | Hx]; auto. right; simpl. rewrite Hx. reflexivity. right; simpl. rewrite Hy. destruct_tests; reflexivity. destruct (IHeval2 _ _ H3) as [HB | Hy]; auto. destruct (IHeval1 _ _ H2) as [HA | Hx]; auto. right; simpl. rewrite Hx, Hy; simpl. reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)