PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
1
2
1
2
1.
n:
Surj(
0
n;
(n
0);
z.0)
By:
Unfold `surject` 0
Generated subgoal:
1
b:
(n
0).
a:(
0
n). (
z.0)(a) = b
About:
b:
(n
0). 
a:(0
n). (
z.0)(a) = b Surj(0n; (n0); z.0) b:(n0). a:(0n). (z.0)(a) = b
