Nuprl - Pf fin_dec

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:T| B(t) }

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

By: Analyze -1 THEN Assert ((f o g)(x) = x)

Generated subgoals:

1 8. x: T
9. B(x)
(f o g)(x) = x

2 8. x: T
9. B(x)
10. (f o g)(x) = x
(f o g)(x) = Id(x) {t:T| B(t) }

About:

1	8. `x:` `T` 9. `B(x)` `(f o g)(x) = x`
2	8. `x:` `T` 9. `B(x)` 10. `(f o g)(x) = x` `(f o g)(x) = Id(x) {t:T\| B(t) }`