Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:. f:n x,y:(1 List)//(x Rl y). Bij(n;x,y:(1 List)//(x Rl y);f)

Applied Tactic: Fold `finite` 0
Generated subgoals:

1. Fin(x,y:(1 List)//(x Rl y))