Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:{1...}. A:
. L:L(A). R:A List 
A List 
.
Fin(A)
EquivRel(A List;x,y.x R y)
1-1-Corresp(
n;x,y:(A List)//(x R y))
(x,y,z:A List. x R y (z @ x) R (z @ y))
(
g:x,y:(A List)//(x R y) 
. l:A List. L l 
(g l))
(m:. 1-1-Corresp(m;x,y:(A List)//(x Rl y))) 
(l:A List. Dec(L l))
Applied Tactic: (D 0 THENM D 0 THENM D 0 THENM Assert 
L 
A List 
...a)
Generated subgoals:1. L A List 2. R:A List A List
Fin(A)
EquivRel(A List;x,y.x R y)
1-1-Corresp(n;x,y:(A List)//(x R y))
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y) . l:A List. L l (g l))
(m:. 1-1-Corresp(m;x,y:(A List)//(x Rl y))) (l:A List. Dec(L l))