Nuprl - Pf lpower

1. Alph: Type
2. L: Alph*
3. n:

(Ln) = if n=0 nil else L @ (Ln-1) fi

By: NatInd 3

Generated subgoals:

1 (L0) = if 0=0 nil else L @ (L0-1) fi

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

About:

1	`(L0) = if 0=0 nil else L @ (L0-1) fi`
2	3. `n:` 4. `0 < n` 5. `(Ln-1) = if n-1=0 nil else L @ (Ln-1-1) fi` `(Ln) = if n=0 nil else L @ (Ln-1) fi`