Level: Lib Thy Top: 1
Hypotheses:

  1. n : {1...}

  2. m : n

  3. E : n n

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

  5. z : x,y:m//(x E y)

Conclusion:

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

Applied Tactic: SetupInclusion 5
Generated subgoals:

1. z = z