Eval
Require Export Subst Seval LOptions MuRec internalize_tac.
Instance term_eva : internalized eva.
Proof with crush.
internalizeR. revert y0. induction y;intros[];recStep P...
-destruct (eva y s)... destruct t0... destruct (eva y t)...
Defined.