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