Level: Lib Thy Top: 2
Hypotheses:

  1. n : {1...}

  2. A :

  3. L : L(A)

  4. L A List

Conclusion:

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: (GenExRepD ...a)
Generated subgoals:

1. m:. 1-1-Corresp(m;x,y:(A List)//(x Rl y))

2. Dec(L l)