Level: Lib Thy Top: 2 1
Hypotheses:

  1. n : {1 + 1...}

  2. E:(n - 1) (n - 1) EquivRel((n - 1);x,y.x E y) (x,y:(n - 1). Dec(x E y)) (m:((n - 1) + 1). 1-1-Corresp(m;i,j:(n - 1)//(i E j)))

  3. E : n n

  4. EquivRel(n;x,y.x E y) (x,y:n. Dec(x E y))

Conclusion:

m:(n + 1). 1-1-Corresp(m;i,j:n//(i E j))

Applied Tactic: (Assert EquivRel((n - 1);x,y.x E y) ...a)
Generated subgoals:

1. EquivRel((n - 1);x,y.x E y)

2. m:(n + 1). 1-1-Corresp(m;i,j:n//(i E j))