Level: Lib Thy Top: 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)

Conclusion:

Trans(x,y:(A List)//(x R y);u,v.u (x,y.z:A List. (g z@x) (g z@y)) v)

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

1. a,b,c:x,y:(A List)//(x R y). (z:A List. (g z@a) (g z@b)) (z:A List. (g z@b) (g z@c)) (z:A List. (g z@a) (g z@c))