Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
Alph,L,n,z.(L
n))
Alph:
L:L(Alph)
n:
True
L(Alph)
Applied Tactic:
ProveOpCombTyping `lang_power_wf`
Generated subgoals:
None
(
Alph,L,n,z.(L
n)) 
Alph:
L:L(Alph) n:
True L(Alph)