At: list quo choice pls 1 1 1 1 1
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:
(g(a)) E (g(a))
By: BackThru 3
Generated subgoals:None
About:
