Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: (UnivCD ...a)
Generated subgoals:

1. z x,y:n//(x E y)

2. EquivRel(m;x,y.x E y)