Nuprl - Pf auto1

1. Dec(l:2*. LangOf(Auto)(l))

n:2. n = 0 (l:2*. LangOf(Auto)(l))

By: Analyze 1

Generated subgoals:

1 1. l:2*. LangOf(Auto)(l)
n:2. n = 0 (l:2*. LangOf(Auto)(l))

2 1. (l:2*. LangOf(Auto)(l))
n:2. n = 0 (l:2*. LangOf(Auto)(l))

About:

1	1. `l:2. LangOf(Auto)(l)` `n:2. n = 0 (l:2. LangOf(Auto)(l))`
2	1. `(l:2. LangOf(Auto)(l))` `n:2. n = 0 (l:2. LangOf(Auto)(l))`