Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. E:Alph List 
Alph List 
.
Fin(Alph) 
EquivRel(Alph List;x,y.x E y) (x,y:Alph List. Dec(x E y))
(
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: UnivCD THENW Auto
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))