proposition: Lemma eval_types n n' m m' x x' x'': eval n m x x' -> eval n' m' x x'' -> (n=n' <-> m=m').
proof: Proof. intro H. revert n' m' x''. induction H; intros n' m' x'' H''. apply eval_one' in H''. subst. reflexivity. apply eval_pls in H'' as (?&?&?&?&?). eauto. apply eval_dot in H'' as (?&?&?&?&?&?). erewrite IHeval1 by eassumption. eauto. apply eval_itr' in H''. subst. reflexivity. apply eval_str' in H''. subst. reflexivity. apply eval_cnv in H'' as (?&?&?). symmetry. eauto. apply eval_var' in H'' as (?&?). subst. now split. Qed.
imports: kleene syntax