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