Nuprl - Pf counter

1. e:
2. L: *
3. n:

||e:(Ln)|| = n||e:L||

By: NatInd 3

Generated subgoals:

1 ||e:(L0)|| = 0||e:L||

2 3. n:
4. 0 < n
5. ||e:(Ln-1)|| = (n-1)||e:L||
||e:(Ln)|| = n||e:L||

About:

1	`\|\|e:(L0)\|\| = 0\|\|e:L\|\|`
2	3. `n:` 4. `0 < n` 5. `\|\|e:(Ln-1)\|\| = (n-1)\|\|e:L\|\|` `\|\|e:(Ln)\|\| = n\|\|e:L\|\|`