Level: Lib Thy Top:
Hypotheses:None
Conclusion:
q:
. 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: D 0 THENA Auto THEN Decide 
0 < q
THENA Auto
Generated subgoals:1. 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)))2. 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)))