Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : Alph List

  3. R : Alph List Alph List

  4. EquivRel(Alph List;x,y.x R y)

  5. x,y,z:Alph List. x R y (z @ x) R (z @ y)

  6. g : x,y:(Alph List)//(x R y)

  7. l:Alph List. L l (g l)

Conclusion:

x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rg y)

Applied Tactic: (QuotEqCD ...a)
Generated subgoals:

1. L L(Alph)

2. EquivRel(Alph List;x,y.x Rl y)

3. EquivRel(Alph List;x,y.x Rg y)

4. Alph List = Alph List

5. x Rl y x Rg y