proposition: Lemma eval_itr n x z: eval n n (x^+) z -> exists x', eval n n x x' /\ z = e_itr x'.
proof: Proof. assert (G: forall m u (z: expr n m), eval n m u z -> forall (H: n=m) x, u=e_itr x -> exists x', eval n n x x' /\ z = eq_rect _ (expr n) (e_itr x') m H). intros m z' H. destruct 1; intros E v Hv; try discriminate. rewrite <-(f_equal ((fun n m (e: syntax.expr _ _ n m) => match e in syntax.expr _ _ n m return syntax.expr _ _ n m with e_itr y => y | x => x end) _ _) Hv). eexists. split. eassumption. now rewrite cmp_eq_rect_eq. intro Hz. apply (G _ _ _ Hz eq_refl _ eq_refl). Qed.
imports: kleene syntax