At: list quo choice pls 1 1 1 1 3
1. q: 
2. E: q*
q*Prop
3. 
a:q*. a E a
4. a,b:q*. (a E b) 
(b E a)
5. a,b,c:q*. (a E b) (b E c) (a E c)
6. x,y:q*. Dec(x E y)
7. f: q*
8. g: q*
9. g o f = Id
10. f o g = Id
11. a:
12. b:
13. c:
14. (g(a)) E (g(b))
15. (g(b)) E (g(c))
(g(a)) E (g(c))
By: FwdThru 5 [14;15]
Generated subgoals:None
About:
