proposition: Lemma eval_pls n m x y z: eval n m (x+y) z -> exists x', eval n m x x' /\ exists y', eval n m y y' /\ z=e_pls x' y'.
proof: Proof. remember (x+y)%ast as z' eqn:E. destruct 1; 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_pls x _ => x | x => x end) _ _) E). 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_pls _ y => y | x => x end) _ _) E). eauto. Qed.
imports: kleene syntax