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. g : x,y:(A List)//(x R y)

  6. L : L(A)

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

  8. x : A List

  9. y : A List

Conclusion:

(z:A List. L (z @ x) L (z @ y)) (z:A List. (g (z @ x)) (g (z @ y)))

Applied Tactic: (Assert L A List THENM RWO "7" 0 ...a)
Generated subgoals:

1. L A List

2. (z:A List. (g (z @ x)) (g (z @ y))) (z:A List. (g (z @ x)) (g (z @ y)))