PrintForm Definitions languages Sections AutomataTheory Doc

At: lang power functionality 1 1 1 1 1 1

1. Alph: Type
2. L: LangOver(Alph)
3. L': LangOver(Alph)
4. n':
5. L = L'
6. 0 = 0
7. 0 = 0

=

By: Unfold `lang_eq` 0

Generated subgoal:

1 l:Alph*. (l) (l)


About:
universeequalintnatural_numberalllistapply