% These can be run after  load1 ();

ev_case_z z (s z) ([x:exp] z) (s z) (ev_z) (ev_s z z (ev_z))
: eval (case z (s z) ([x:exp] z)) (s z).

ev_case_z z (s z) ([x:exp] z) (s z) (ev_z) (ev_s z z (ev_z))
: A.

ev_case_z E1 E2 E3 V (ev_z) (ev_s E' V' (ev_z)) : A.

ev_case_z E1 E2 E3 V : A.