PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
T:Type, t:T. Fin(T)
Fin(T
T)
By:
Unfold `finite` 0
THEN
ExRepD
Generated subgoal:
1
1.
T:
Type
2.
t:
T
3.
n:
4.
f:
n
T
5.
Bij(
n; T; f)
n:
, f:(
n
T
T). Bij(
n; T
T; f)
About:
n
Tn; T; f)
n:, f:(nT
T). Bij(n; TT; f) 
T:Type, t:T. Fin(T) 
Fin(TT)nTn; T; f) n:, f:(nTT). Bij(n; TT; f)
