Nuprl - Pf multiply_functionality_wrt

1. i1:
2. i2:
3. j1:
4. j2:
5. i1j1
6. i2j2

i1i2j1j2

By: Using [`n',i1] (FwdThru Thm* a,b:, n:. ab nanb [6])

Generated subgoal:

1 7. i1i2i1j2
i1i2j1j2

About: