Level: Lib Thy Top: 1 1
Hypotheses:

  1. A :

  2. R : A List A List

  3. EquivRel(A List;x,y.x R y)

  4. x,y,z:A List. x R y (z @ x) R (z @ y)

  5. z : A List

  6. y1 : A List

  7. y2 : A List

  8. y1 R y2

Conclusion:

z@y1 = z@y2

Applied Tactic: (Unfold `mn_quo_append` 0 THENM EqTypeCD THENM BHyp 4 ...)
Generated subgoals:

None