At: quo of quo 1 2 1
1. T: Type
2. R: T
TProp
3. EquivRel x,y:T. x R y
4. Q: (x,y:T//(x R y))(x,y:T//(x R y))Prop
5. EquivRel u,v:x,y:T//(x R y). u Q v
6. EquivRel x,y:T. x Q y
7. x: x,y:T//(x Q y)
x 
u,v:(x,y:T//(x R y))//(u Q v)
By:
Unfold `member` 0
THEN
Analyze 7
THEN
Analyze
Generated subgoals:None
About:
