Nuprl - Pf add_mono_wrt

a,b,n:. ab a+nb+n

By: GenUnivCD

Generated subgoals:

1 1. a:
2. b:
3. n:
4. ab
a+nb+n

2 1. a:
2. b:
3. n:
4. a+nb+n
ab

About:

1	1. `a:` 2. `b:` 3. `n:` 4. `ab` `a+nb+n`
2	1. `a:` 2. `b:` 3. `n:` 4. `a+nb+n` `ab`