Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. R:T 
T 
.
EquivRel(T;x,y.x R y)
(Q:x,y:T//(x R y) x,y:T//(x R y)
EquivRel(x,y:T//(x R y);u,v.u Q v) EquivRel(T;x,y.x Q y))
Applied Tactic: (UnivCD ...a)
Generated subgoals:1. EquivRel(T;x,y.x Q y)