PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dec
fin
1
1
1
1
2
1.
T:
Type
2.
B:
T
Prop
3.
f:
0
T
4.
g:
T
0
5.
g o f = Id
6.
f o g = Id
7.
t:T. Dec(B(t))
8.
x:
T
9.
B(x)
10.
(f o g)(x) = x
(f o g)(x) = Id(x)
{t:T| B(t) }
By:
Reduce -1
THEN
Reduce 0
THEN
Analyze
Generated subgoal:
1
10.
f(g(x)) = x
B(f(g(x)))
About:
B(f(g(x)))
Prop
0T0
t:T. Dec(B(t)) (f o g)(x) = Id(x) 
{t:T| B(t) } B(f(g(x)))
