()
| 479 | /// `imax(_, 0) = 0`. |
| 480 | #[test] |
| 481 | fn level_imax_zero_second_arg() { |
| 482 | let u = p("u"); |
| 483 | let lean = im(u, z()); |
| 484 | let aux_gen = z(); |
| 485 | assert!(level_alpha_eq(&lean, &aux_gen).is_ok()); |
| 486 | } |
| 487 | |
| 488 | /// Nested `max` absorption: `max(a, max(a, b)) = max(a, b)`. |
| 489 | #[test] |