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