Level:
Lib
Thy
Top
:
1
Hypotheses:
q :
Conclusion:
1-1-Corresp(
q List;
)
Applied Tactic:
RWH (RevLemmaC `bij_iff_1_1_corr`) 0 THENA Auto
Generated subgoals:
1
.
f:
q List
. Bij(
q List;
;f)
1-1-Corresp(q List;)
f:q List 
. Bij(q List;;f)