Nuprl - Proof: imax assoc 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: imax assoc 1

1. a :

2. b :

3. c :

imax(a;imax(b;c)) = imax(imax(a;b);c)

By:	Decide: ab \| bc THEN 2 Times (ElimImaxmin Auto 0)

Generated subgoals:

1 4. ab
5. bc
  c = c
Trivial

2 4. ab
5. bc
  b = b
Trivial

3 4. ab
5. bc
  imax(a;c) = imax(a;c)
Auto

4 4. ab
5. bc
  a = a
Trivial

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html