Ad
  • Custom User Avatar
    • The initial body cannot be reduced.
    • Only match-reduction could be enabled by replacing n with a concrete value (e.g. S (S O)), but n is not being matched, so still no reduction is available. So, e.g., strange 0 and strange 1 are obviously not alpha-convertible. (Try using "Compute strange 0" to see.)
    • But replacing u with tt does enable match-reduction, yielding (fun _ => tt) n, followed by beta-reduction, to give just tt.