PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
1
2
1.
n:
Bij(
0
n;
(n
0);
z.0)
By:
Unfold `biject` 0
Generated subgoal:
1
Inj(
0
n;
(n
0);
z.0) & Surj(
0
n;
(n
0);
z.0)
About:
Inj(
0
n; (n
0); 
z.0) & Surj(0n; (n0); z.0) Bij(0n; (n0); z.0) Inj(0n; (n0); z.0) & Surj(0n; (n0); z.0)
