PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dist
func
1
1
1.
St:
Type
2.
n:
3.
f:(
n
St). Bij(
n; St; f)
eq:(St
St
).
x,y:St. eq(x,y)
x = y
By:
RWH (LemmaC
Thm*
(
f:(A
B). Bij(A; B; f))
(A ~ B)) 3
Generated subgoal:
1
3.
n ~ St
eq:(St
St
).
x,y:St. eq(x,y)
x = y
About:
n ~ St
eq:(St
St
). 
x,y:St. eq(x,y) 
x = yf:(nSt). Bij(n; St; f) eq:(StSt). x,y:St. eq(x,y) x = yf:(AB). Bij(A; B; f)) 
(A ~ B))
3n ~ St eq:(StSt). x,y:St. eq(x,y) x = y
