Nuprl - Pf lang_prod_sing 1 1 2 2 2 1 2

1. Alph: Type
2. L: Alph*Prop
3. l: Alph*
4. L(l)
5. ||l[||l||..||l||]|| = 0

(l[||l||..||l||]) = nil

By: Assert (m:Alph*. ||m|| = 0 m = nil)

Generated subgoals:

1 m:Alph*. ||m|| = 0 m = nil

2 6. m:Alph*. ||m|| = 0 m = nil
(l[||l||..||l||]) = nil

About:

1	`m:Alph*. \|\|m\|\| = 0 m = nil`
2	6. `m:Alph*. \|\|m\|\| = 0 m = nil` `(l[\|\|l\|\|..\|\|l\|\|]) = nil`