Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. E:T T . EquivRel(T;x,y.E[x;y]) (x,y:T. Dec(E[x;y])) (u,v:x,y:T//E[x;y]. Dec(u = v))
Applied Tactic: (RepeatMFor 4 (D 0) ...a)
Generated subgoals:

1. u,v:x,y:T//E[x;y]. Dec(u = v)