Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(St)

Conclusion:

n:. #(St)=n

Applied Tactic: (D 4 THEN RWH (LemmaC `bij_iff_1_1_corr`) 5 THENM InstLemma `one_one_sym` [n;St] ...a)
Generated subgoals:

1. n:. #(St)=n