PrintForm Definitions languages Sections AutomataTheory Doc

At: apply functionality wrt lang eq 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')

By: RWH (HypC 7) 0

Generated subgoal:

1 L(l') L'(l')


About:
applyuniverselistfunctionpropallequal