proposition: Lemma eval_fun n m x x' x'': eval n m x x' -> eval n m x x'' -> x'=x''.
proof: Proof. induction 1; intro H'. now apply eval_one in H'. apply eval_pls in H' as (?&?&?&?&->). firstorder congruence. apply eval_dot in H' as (q&?&?&?&?&->). assert(m=q) by eauto using eval_types_l. subst. firstorder congruence. apply eval_itr in H' as (?&?&->). firstorder congruence. apply eval_str in H' as (?&?&->). firstorder congruence. apply eval_cnv in H' as (?&?&->). firstorder congruence. apply eval_var in H'. congruence. Qed.
imports: kleene syntax