Level: Lib Thy Top: 2 1
Hypotheses:

  1. q :

  2. (0 < q)

  3. E : q List q List

  4. EquivRel(q List;x,y.x E y) (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: With Id (D 0) THENA Auto
Generated subgoals:

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