Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph:. L:L(Alph). (L0) =

Applied Tactic: RecCaseSplit `lang_power` THEN Auto
Generated subgoals:

1. =