PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin dec fin 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))

f o g = Id {t:T| B(t) }{t:T| B(t) }

By: Ext

Generated subgoal:

18. x: {t:T| B(t) }
(f o g)(x) = Id(x) {t:T| B(t) }


About:
equalfunctionsetapplyuniversepropnatural_numberall