Nuprl - Pf counter

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

||e:L @ M|| = ||e:L||+||e:M||

By: ListInd 2

Generated subgoals:

1 ||e:nil @ M|| = ||e:nil||+||e:M||

2 4. u:
5. v: *
6. ||e:v @ M|| = ||e:v||+||e:M||
||e:(u.v) @ M|| = ||e:u.v||+||e:M||

About:

1	`\|\|e:nil @ M\|\| = \|\|e:nil\|\|+\|\|e:M\|\|`
2	4. `u:` 5. `v:` `*` 6. `\|\|e:v @ M\|\| = \|\|e:v\|\|+\|\|e:M\|\|` `\|\|e:(u.v) @ M\|\| = \|\|e:u.v\|\|+\|\|e:M\|\|`