proposition: Lemma eval_cnv n m x z: eval n m (x°) z -> exists x', eval m n x x' /\ z=e_cnv x'.
proof: Proof. remember (x°)%ast as z' eqn:E. destruct 1; try discriminate. rewrite <- (f_equal ((fun n m (e: syntax.expr _ _ n m) => match e with e_cnv x => x | _ => e_zer _ _ end) _ _) E). eauto. Qed.
imports: kleene syntax