PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
6
1
1
1
1
1
1
1
1.
T:
Type
2.
R:
T
Prop
3.
(
f:(
0
T). Bij(
0; T; f)) & (
t:T. Dec(R(t)))
Dec(
t:T. R(t))
By:
Analyze 3
Generated subgoal:
1
3.
f:(
0
T). Bij(
0; T; f)
4.
t:T. Dec(R(t))
Dec(
t:T. R(t))
About:
f:(
0
T). Bij(0; T; f)
t:T. Dec(R(t))
Dec(t:T. R(t))Propf:(0T). Bij(0; T; f)) & (t:T. Dec(R(t))) Dec(t:T. R(t))f:(0T). Bij(0; T; f)t:T. Dec(R(t)) Dec(t:T. R(t))
