Level: Lib Thy Top: 2 1
Hypotheses:

  1. n : {1...}

  2. A :

  3. L : L(A)

  4. L A List

  5. R : A List A List

  6. Fin(A)

  7. EquivRel(A List;x,y.x R y)

  8. 1-1-Corresp(n;x,y:(A List)//(x R y))

  9. x,y,z:A List. x R y (z @ x) R (z @ y)

  10. g : x,y:(A List)//(x R y)

  11. l:A List. L l (g l)

Conclusion:

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

Applied Tactic: (Assert x,y:x,y:(A List)//(x R y). Dec(x Rg y) ...a)
Generated subgoals:

1. Dec(x Rg y)

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