Level: Lib Thy Top: 2
Hypotheses:

  1. q :

  2. (0 < q)

Conclusion:

E:q List q List EquivRel(q List;x,y.x E y) (x,y:q List. Dec(x E y)) (h:q List q List. (x,y:q List. x E y h x = h y) (x:q List. x E (h x)))

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

1. h:q List q List. (x,y:q List. x E y h x = h y) (x:q List. x E (h x))