Nuprl - Pf lang_sing

Alph:Type, L:LangOver(Alph). (L) = L

By: Unfold `languages` 0 THEN Unfold `lang_prod` 0 THEN Unfold `lang_sing` 0 THEN Unfold `lang_eq` 0 THEN UnivCD

Generated subgoal:

1 1. Alph: Type
2. L: Alph*Prop
3. l: Alph*
(l.i:{0...||l||}. (l.null(l))(l[0..i]) & L(l[i..||l||]))(l) L(l)

About: