Nuprl - Pf lpower_alt 1 2 2 1 2

1. Alph: Type
2. L: Alph*
3. n:
4. 0 < n
5. (Ln-1) = if n-1=0 nil else L @ (Ln-1-1) fi
6. n = 0
7. n-1 = 0

(Ln) = (L @ (Ln-1-1) @ L)

By: Assert ((Ln-1) = (L @ (Ln-1-1)))

Generated subgoals:

1 (Ln-1) = (L @ (Ln-1-1))

2 8. (Ln-1) = (L @ (Ln-1-1))
(Ln) = (L @ (Ln-1-1) @ L)

About:

1	`(Ln-1) = (L @ (Ln-1-1))`
2	8. `(Ln-1) = (L @ (Ln-1-1))` `(Ln) = (L @ (Ln-1-1) @ L)`