fun is_n_redex (LAM (x, APP(m, x'))) = if (ID x)=x' andalso not (contains x (freeVars m)) then true
                                       else false
  | is_n_redex (_)                   = false;

fun has_n_redex (APP (m, n)) = has_n_redex m orelse has_n_redex n
  | has_n_redex (LAM (x, m)) = if is_n_redex (LAM (x, m)) then true
                               else has_n_redex m
  | has_n_redex (ID x)       = false;


fun fst (APP (m, n)) = m;
fun n_reduce (APP (m, n)) = if has_n_redex m      then APP (n_reduce m, n)
                            else if has_n_redex n then APP (m, n_reduce n)
                                                  else APP (m,n)
  | n_reduce (LAM (x, m)) = if is_n_redex (LAM (x, m)) then fst m
                            else LAM (x, n_reduce m)
  | n_reduce (ID x)       = (ID x);