PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
iff
1
1
nsub
T:Type. Fin(T)
(
m:
.
m ~ T)
By:
Unfold `finite` 0
THEN
UnivCD
Generated subgoal:
1
1.
T:
Type
(
n:
, f:(
n
T). Bij(
n; T; f))
(
m:
.
m ~ T)
About:
(
n:
, f:(n
T). Bij(n; T; f)) 
(m:. m ~ T) 
T:Type. Fin(T) (m:. m ~ T) (n:, f:(nT). Bij(n; T; f)) (m:. m ~ T)
