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: UnivCD THENW Auto THEN D 3
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))