Level: Lib Thy Top: 1 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(Alph) Fin(St)

  5. x : Alph List

  6. y : Alph List

  7. n :

  8. f:n x,y:(Alph List)//(x Rl y). Bij(n;x,y:(Alph List)//(x Rl y);f)

Conclusion:

Dec(x = y)

Applied Tactic: InstLemma `lang_rel_equi` [Alph;L(Auto) ] THENA Auto THEN RWH (LemmaC `bij_iff_1_1_corr`) 8 THENA Auto
Generated subgoals:

1. Dec(x = y)