Level: Lib Thy Top: 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)

Conclusion:

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

Applied Tactic: (FLemma `bij_iff_1_1_corr` [4] THENM D (-1) ...a)
Generated subgoals:

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