Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:
2. n = 0 
(l:2 List. L(Auto
) l)
Applied Tactic: InstLemma `empty_lang_dec` [
2
;3;Auto] THENA (Auto THEN BLemma `nsub_is_finite` THEN Auto)
Generated subgoals:1. n:2. n = 0 (l:2 List. L(Auto) l)