PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dec
fin
1
1
1.
T:
Type
2.
B:
T
Prop
3.
f:
0
T
4.
g:
T
0
5.
InvFuns(
0; T; f; g)
6.
t:T. Dec(B(t))
InvFuns(
0; {t:T| B(t) }; f; g)
By:
Unfold `inv_funs` 0
THEN
Unfold `inv_funs` 5
THEN
Analyze 0
Generated subgoal:
1
5.
g o f = Id
6.
f o g = Id
7.
t:T. Dec(B(t))
f o g = Id
{t:T| B(t) }
{t:T| B(t) }
About:
t:T. Dec(B(t))
f o g = Id 
{t:T| B(t) }
{t:T| B(t) }Prop
0T00; T; f; g)t:T. Dec(B(t)) InvFuns(0; {t:T| B(t) }; f; g)t:T. Dec(B(t)) f o g = Id {t:T| B(t) }{t:T| B(t) }
