proposition: Lemma eval_one n z: eval n n 1 z -> z=e_one n.
proof: Proof. assert (G: forall m u (z: expr n m), eval n m u z -> forall (H: n=m), u=e_one _ -> z = eq_rect _ (expr n) (e_one n) m H). intros m z' H. destruct 1; intros; try discriminate. now rewrite cmp_eq_rect_eq. intro Hz. apply (G _ _ _ Hz eq_refl eq_refl). Qed.
imports: kleene syntax