At: mn quo append wf 1 1
1. A: Type
2. R: A*
A*Prop
3. EquivRel x,y:A*. x R y
4. 
x,y,z:A*. (x R y) 
((z @ x) R (z @ y))
5. z: A*
6. y1: A*
7. y2: A*
8. y1 R y2
z@
y1 = z@y2 
x,y:A*//(x R y)
By:
Unfold `mn_quo_append` 0
THEN
Analyze
THEN
BackThru 4
Generated subgoals:None
About:
