Level: Lib Thy Top: 1
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: InstLemma `list_quo_choice_pls` [q] THEN Auto
Generated subgoals:

None