proposition: Lemma syntax_eval_id n m (e: expr n m): syntax.eval (X:=u_ops) (f':=fun _ => tt) (@e_var _ _ _) (erase e) = erase e.
proof: Proof. induction e; simpl; unfold str; simpl; repeat f_equal; assumption. Qed.
imports: kleene syntax