Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

q:. n1,n2:. r1:(qn1). r2:(qn2). (qn1) + r1 = (qn2) + r2 n1 = n2 r1 = r2

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. n1 = n2 r1 = r2