Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. E : T T

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

  4. x : T

  5. y : T

  6. x = y

Conclusion:

x = y

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

1. x E y