Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:{1...}. E:
n 
n 
.
EquivRel(n;i,j.i E j) 
(x:i,j:n//(i E j). 
(x = n - 1) x 
i,j:(n - 1)//(i E j))
Applied Tactic: (UnivCD ...a)
Generated subgoals:1. x i,j:(n - 1)//(i E j)2. n - 1 i,j:n//(i E j)