Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. R:Alph List 
Alph List 
.
Fin(Alph)
EquivRel(Alph List;x,y.x R y)
Fin(x,y:(Alph List)//(x R y))
(x,y,z:Alph List. x R y (z @ x) R (z @ y))
(g:x,y:(Alph List)//(x R y) 
. x,y:x,y:(Alph List)//(x R y). Dec(x Rg y))
Applied Tactic: (RepeatFor 7 (Id THENM D 0) ...a)
Generated subgoals:1. x,y:x,y:(Alph List)//(x R y). Dec(x Rg y)