Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. E : Alph List Alph List

  3. Fin(Alph) EquivRel(Alph List;x,y.x E y) (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 THEN D 4
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))