Nuprl - Pf add_mono_wrt

a,b,n:. a = b a+n = b+n

By: GenUnivCD

Generated subgoals:

1 1. a:
2. b:
3. n:
4. a = b
a+n = b+n

2 1. a:
2. b:
3. n:
4. a+n = b+n
a = b

About:

1	1. `a:` 2. `b:` 3. `n:` 4. `a = b` `a+n = b+n`
2	1. `a:` 2. `b:` 3. `n:` 4. `a+n = b+n` `a = b`