Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:{1...}. A:
. R:A 
A 
.
1-1-Corresp(
n;A)
EquivRel(A;x,y.x R y)
(x,y:A. Dec(x R y))
(
m:(n + 1). 1-1-Corresp(m;x,y:A//(x R y)))
Applied Tactic: (UnivCD ...a)
Generated subgoals:1. m:(n + 1). 1-1-Corresp(m;x,y:A//(x R y))