Level:
Lib
Thy
Top
:
1
1
Hypotheses:
n : {1...}
E :
n
n
EquivRel(
n;i,j.i E j)
x : i,j:
n//(i E j)
(x = n - 1)
EquivRel(
(n - 1);x,y.x E y)
Conclusion:
x
i,j:
(n - 1)//(i E j)
Applied Tactic:
(QuotD 4 ...a)
Generated subgoals:
1
. x1 = x2
n 
n 
n;i,j.i E j)n//(i E j)
(x = n - 1)(n - 1);x,y.x E y)
x 
i,j:(n - 1)//(i E j)