PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
nsub
is
finite
1
1
1
1
2
1.
n:
Surj(
n;
n; Id)
By:
Unfold `surject` 0
Generated subgoal:
1
b:
n.
a:
n. Id(a) = b
About:
b:
n. 
a:n. Id(a) = b Surj(n; n; Id) b:n. a:n. Id(a) = b
