PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
2
1
1
1
1
1
1
1
2
1
1.
n:
2.
0 < n
3.
T:
Type
4.
R:
T
Prop
5.
f:
n
T
6.
Bij(
n; T; f)
7.
t:T. Dec(R(t))
Inj(
(n-1); {t:T|
t = f(n-1) }; f)
By:
Unfold `inject` 0
Generated subgoal:
1
a1,a2:
(n-1). f(a1) = f(a2)
{t:T|
t = f(n-1) }
a1 = a2
About:
a1,a2:
(n-1). f(a1) = f(a2) 
{t:T| 
t = f(n-1) } 
a1 = a2
PropnTn; T; f)t:T. Dec(R(t)) Inj((n-1); {t:T| t = f(n-1) }; f) a1,a2:(n-1). f(a1) = f(a2) {t:T| t = f(n-1) } a1 = a2
