Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. E : T T

  3. x : T

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

Conclusion:

x x,y:T//(x E y)

Applied Tactic: Auto
Generated subgoals:

None