Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. n :

Conclusion:

(Ln) L(Alph)

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

None