Level:
Lib
Thy
Top
:
1
Hypotheses:
q :
n :
i :
Conclusion:
(q
n
)
(q
n + i
)
Applied Tactic:
NatInd 3 THENA Auto
Generated subgoals:
1
.
(q
n
)
(q
n + 0
)
2
.
(q
n
)
(q
n + i
)
(q
n
) 
(qn + i)(qn) (qn + 0)(qn) (qn + i)