Nuprl - Pf counter_append 1 2 1 1 1 1 1

1. e:
2. L: *
3. M: *
4. u:
5. v: *
6. ||e:v @ M|| = ||e:v||+||e:M||
7. e = u

1+||e:v @ M|| = if e=u 1+||e:v|| else ||e:v|| fi+||e:M||

By: SplitOnConclITE

Generated subgoals:

1 8. e = u
1+||e:v @ M|| = 1+||e:v||+||e:M||

2 8. e = u
1+||e:v @ M|| = ||e:v||+||e:M||

About:

1	8. `e = u` `1+\|\|e:v @ M\|\| = 1+\|\|e:v\|\|+\|\|e:M\|\|`
2	8. `e = u` `1+\|\|e:v @ M\|\| = \|\|e:v\|\|+\|\|e:M\|\|`