Level:
Lib
Thy
Top
:
1
1
Hypotheses:
St :
n :
f:
n
St. Bij(
n;St;f)
Conclusion:
eq:St
St
.
x,y:St.
(eq x y)
x = y
Applied Tactic:
(RWH (LemmaC `bij_iff_1_1_corr`) 3 ...a)
Generated subgoals:
1
.
eq:St
St
.
x,y:St.
(eq x y)
x = y
f:n 
St. Bij(n;St;f)
eq:St St 
. 
x,y:St. 
(eq x y) 
x = yeq:St St . x,y:St. (eq x y) x = y