PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
is
decid
1
1
1
1
1
1.
T:
Type
2.
n:
3.
f:
n
T
4.
a1,a2:
n. f(a1) = f(a2)
a1 = a2
5.
Surj(
n; T; f)
6.
x:
T
7.
y:
T
Dec(x = y)
By:
Unfold `surject` 5
Generated subgoal:
1
5.
b:T.
a:
n. f(a) = b
6.
x:
T
7.
y:
T
Dec(x = y)
About:
b:T. 
a:
n. f(a) = b
Dec(x = y)n
Ta1,a2:n. f(a1) = f(a2) 
a1 = a2n; T; f) Dec(x = y)b:T. a:n. f(a) = b Dec(x = y)
