Level: Lib Thy Top: 1
Hypotheses:

  1. n : {1...}

  2. m : n

  3. E : n n

  4. EquivRel(n;i,j.i E j)

Conclusion:

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

Applied Tactic: (Assert EquivRel(m;i,j.i E j) ...a)
Generated subgoals:

1. EquivRel(m;i,j.i E j)

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