PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dec fin 1 1 1 1 1

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)

(f o g)(x) = x

By:
RWH (HypC 6) 0
THEN
Reduce 0


Generated subgoals:

None


About:
equalapplyuniversefunctionpropnatural_numberall