PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one one preser fin

T,S:Type. Fin(T) & (T ~ S) Fin(S)
By:
Unfold `finite` 0
THEN
Unfold `one_one_corr` 0
THEN
UnivCD
Generated subgoal:

11. T: Type
2. S: Type
3. (n:, f:(nT). Bij(n; T; f)) & (f:(TS), g:(ST). InvFuns(T; S; f; g))
n:, f:(nS). Bij(n; S; f)

About:
alluniverseimpliesandexistsfunctionnatural_number