PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dec fin 1 1 1 1 2

1. T: Type
2. B: TProp
3. f: 0T
4. g: T0
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:

110. f(g(x)) = x
B(f(g(x)))


About:
equalsetapplyuniversefunctionpropnatural_numberall