Level: Lib Thy Top:
Hypotheses:None
Conclusion:
A,B:
. f:A 
B. R:B B 
.
Bij(A;B;f)
EquivRel(B;x,y.x R y)
(
F:x,y:A//(x R_f y) x,y:B//(x R y). Bij(x,y:A//(x R_f y);x,y:B//(x R y);F))
Applied Tactic: (UnivCD ...a)
Generated subgoals:1. F:x,y:A//(x R_f y) x,y:B//(x R y). Bij(x,y:A//(x R_f y);x,y:B//(x R y);F)