Nuprl - Pf ndiff_ndiff 1 1 1 1

1. a:
2. b:
3. c:

imax(a+-b+-c;imax(0+-c;0)) = imax(a+-b+-c;0)

By: RWN 2 (UnfoldTopC `imax`) 0 THEN SplitOnConclITE

Generated subgoals:

1 4. 0+-c0
imax(a+-b+-c;0) = imax(a+-b+-c;0)

2 4. 0 < 0+-c
imax(a+-b+-c;0+-c) = imax(a+-b+-c;0)

About:

1	4. `0+-c0` `imax(a+-b+-c;0) = imax(a+-b+-c;0)`
2	4. `0 < 0+-c` `imax(a+-b+-c;0+-c) = imax(a+-b+-c;0)`