At: en inj 1 2 1 2 2 1 1 1 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. u: n
6. v: n*
7. u1: n
8. v1: n*
9. ||u.v|| = m & ||u1.v1|| = m
10. u+en(v)
n = u1+en(v1)n
11. u = u1 & en(v) = en(v1)
u.v = u1.v1
By: Analyze
Generated subgoals:| 1 | u = u1 |
| 2 | v = v1 |
About:
