Level: Lib Thy Top: 1 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 E y

Applied Tactic: (Unfolds ``equiv_rel`` 3 THENM Unfold `refl` 3 THENM D 3 ...a)
Generated subgoals:

1. x E y