Nuprl - Pf apply_functionality_wrt_lang

Alph:Type, l,l':Alph*, L,L':LangOver(Alph). L = L' l = l' (L(l) L'(l'))

By: Unfold `languages` 0 THEN Unfold `lang_eq` 0 THEN UnivCD THEN Reduce 0

Generated subgoal:

1 1. Alph: Type
2. l: Alph*
3. l': Alph*
4. L: Alph*Prop
5. L': Alph*Prop
6. l:Alph*. L(l) L'(l)
7. l = l'
L(l) L'(l')

About: