PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
1
1
1
1
1
1
1
1
1
1
1.
T:
Type
2.
R:
T
Prop
3.
f:
0
T
4.
Inj(
0; T; f)
5.
b:T.
a:
0. f(a) = b
6.
t:T. Dec(R(t))
7.
t:
T
8.
R(t)
False
By:
Witness5 t
Generated subgoal:
1
5.
t:T. Dec(R(t))
6.
t:
T
7.
R(t)
8.
a:
0. f(a) = t
False
About:
t:T. Dec(R(t))
a:
0. f(a) = t
False
Prop0T0; T; f)b:T. a:0. f(a) = bt:T. Dec(R(t)) Falset:T. Dec(R(t))a:0. f(a) = t False
