Nuprl - Pf incl_aux3

1. n: {1...}
2. m: n
3. E: nnProp
4. EquivRel i,j:n. i E j

x,y:i,j:m//(i E j). x = y i,j:n//(i E j) x = y

By: Assert (EquivRel i,j:m. i E j)

Generated subgoals:

1 EquivRel i,j:m. i E j

2 5. EquivRel i,j:m. i E j
x,y:i,j:m//(i E j). x = y i,j:n//(i E j) x = y

About:

1	`EquivRel i,j:m. i E j`
2	5. `EquivRel i,j:m. i E j` `x,y:i,j:m//(i E j). x = y i,j:n//(i E j) x = y`