Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. E:T 
T 
.
EquivRel(T;x,y.E[x;y])
(F:x,y:T//E[x;y]
(w:x,y:T//E[x;y]. SqStable(F w)) ((z:x,y:T//E[x;y]. F[z]) 
(z:T. F[z])))
Applied Tactic: Unfold `so_apply` 0
Generated subgoals:1. T:. E:T T .
EquivRel(T;x,y.E x y)
(F:x,y:T//(E x y)
(w:x,y:T//(E x y). SqStable(F w)) ((z:x,y:T//(E x y). F z) (z:T. F z)))