Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
q,n,i:
.
(q
n
)
(q
n + i
)
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
.
(q
n
)
(q
n + i
)
q,n,i:
. 
(q
n
) 
(qn + i)(qn) (qn + i)