Level: Lib Thy Top: 1
Hypotheses:

  1. q :

  2. E : q List q List

  3. EquivRel(q List;x,y.x E y)

  4. x,y:q List. Dec(x E y)

Conclusion:

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: InstLemma `list_1_1_nat` [q] 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))