1 | 8. l: Alph* 9. ||l|| = n@0 10. ||l|| < n n 11. a': Alph* 12. ||a'|| < ||l|| & R((l @ b),a' @ b) & R((l @ c),a' @ c) 13. ||a'|| < n@0  ( a'@0:Alph*. ||a'@0|| < n n & R((a' @ b),a'@0 @ b) & R((a' @ c),a'@0 @ c)) a':Alph*. ||a'|| < n n & R((l @ b),a' @ b) & R((l @ c),a' @ c) |