PrintForm Definitions languages Sections AutomataTheory Doc

At: lang eq transitivity 1
1. Alph: Type
2. L: Alph*Prop
3. M: Alph*Prop
4. N: Alph*Prop
5. l:Alph*. L(l) M(l)
6. l:Alph*. M(l) N(l)
7. l: Alph*

L(l) N(l)
By: RWH (HypC 5) 0
Generated subgoal:

1 M(l) N(l)

About:
applyuniversefunctionlistpropall