At: list quo choice 2 1 1 1 1 2
1. q: 
2. 
0 < q
3. E: q*
q*Prop
4. (EquivRel x,y:q*. x E y) & (
x,y:q*. Dec(x E y))
5. q = 0
x:q*. x E (Id(x))
By:
Reduce 0
THEN
Analyze 4
THEN
Unfold `equiv_rel` 4
THEN
Analyze 4
THEN
Unfold `refl` 4
Generated subgoals:None
About:
