Level: Lib Thy Top: 1 1
Hypotheses:

  1. n : {1...}

  2. A :

  3. R : A A

  4. 1-1-Corresp(n;A)

  5. EquivRel(A;x,y.x R y)

  6. x,y:A. Dec(x R y)

  7. f : n A

  8. Bij(n;A;f)

Conclusion:

m:(n + 1). 1-1-Corresp(m;x,y:A//(x R y))

Applied Tactic: (FLemma `quotient_1_1_corr` [5;8] ...a)
Generated subgoals:

1. m:(n + 1). 1-1-Corresp(m;x,y:A//(x R y))