Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. R : Alph List Alph List

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

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

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

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

  8. x : Alph List

  9. y : Alph List

  10. x R y

Conclusion:

x Rl y

Applied Tactic: (Unfold `lang_rel` 0 THENM Reduce 0 ...a)
Generated subgoals:

1. z:Alph List. L (z @ x) L (z @ y)