Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:{1...}. m:n. E:n n . EquivRel(n;i,j.i E j) (x,y:i,j:m//(i E j). x = y x = y)

Applied Tactic: (D 0 THENM D 0 THENM D 0 THENM D 0 ...a)
Generated subgoals:

1. x,y:i,j:m//(i E j). x = y x = y