At: fin alph list quo 1 1 1 1 1 1 3
1. Alph: Type
2. E: Alph*
Alph*Prop
3. n: 
4. f: nAlph
5. g: Alphn
6. InvFuns(n; Alph; f; g)
7. 
a:Alph*. a E a
8. a,b:Alph*. (a E b) 
(b E a)
9. a,b,c:Alph*. (a E b) (b E c) (a E c)
10. x,y:Alph*. Dec(x E y)
11. a: n*
12. b: n*
13. c: n*
14. map(f;a) E map(f;b)
15. map(f;b) E map(f;c)
map(f;a) E map(f;c)
By: FwdThru 9 [14;15]
Generated subgoals:None
About:
