Nuprl - Pf lang_auto

1. Alph: Type
2. L: LangOver(Alph)
3. EquivRel x,y:Alph*. x L-induced Equiv y

g:((x,y:Alph*//(x L-induced Equiv y))). (l:Alph*. L(l) g(l)) LangOf(A(g)) = L

By: Assert (L Alph*Prop)

Generated subgoals:

1 L Alph*Prop

2 4. L Alph*Prop
g:((x,y:Alph*//(x L-induced Equiv y))). (l:Alph*. L(l) g(l)) LangOf(A(g)) = L

About:

1	`L Alph*Prop`
2	4. `L AlphProp` `g:((x,y:Alph//(x L-induced Equiv y))). (l:Alph*. L(l) g(l)) LangOf(A(g)) = L`