Nuprl - Pf counter_append 1 2 1

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

if null((u.v) @ M)0 ;e=hd(((u.v) @ M))1+||e:tl(((u.v) @ M))|| else ||e:tl(((u.v) @ M))|| fi = ||e:u.v||+||e:M||

By: Reduce 0

Generated subgoal:

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

About: