Nuprl - Pf en_inj 1 2 1

1. n:
2. m:
3. 0 < m
4. l1,l2:n*. ||l1|| = m-1 & ||l2|| = m-1 en(l1) = en(l2) l1 = l2
5. l1: n*
6. l2: n*

||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2

By: Analyze 5

Generated subgoals:

1 ||nil|| = m & ||l2|| = m en(nil) = en(l2) nil = l2

2 7. u: n
8. v: n*
||u.v|| = m & ||l2|| = m en(u.v) = en(l2) u.v = l2

About:

1	`\|\|nil\|\| = m & \|\|l2\|\| = m en(nil) = en(l2) nil = l2`
2	7. `u:` `n` 8. `v:` `n*` `\|\|u.v\|\| = m & \|\|l2\|\| = m en(u.v) = en(l2) u.v = l2`