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)
1-1-Corresp(x,y:T//(x Q y);u,v:x,y:T//(x R y)//(u Q v)))
Applied Tactic: (UnivCD THENM Unfold `one_one_corr` 0 ...a)
Generated subgoals:1. 
f:x,y:T//(x Q y) u,v:x,y:T//(x R y)//(u Q v)
g:u,v:x,y:T//(x R y)//(u Q v) x,y:T//(x Q y)
InvFuns(x,y:T//(x Q y);u,v:x,y:T//(x R y)//(u Q v);f;g)