Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. E : Alph List Alph List

  3. Fin(Alph)

  4. EquivRel(Alph List;x,y.x E y)

  5. x,y:Alph List. Dec(x E y)

Conclusion:

h:Alph List Alph List. (x,y:Alph List. x E y h x = h y) (x:Alph List. x E (h x))

Applied Tactic: D 3
Generated subgoals:

1. h:Alph List Alph List. (x,y:Alph List. x E y h x = h y) (x:Alph List. x E (h x))