Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n1,n2,k1,k2:. n1 = n2 k1 = k2 (n1k1) = (n2k2)

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. (n1k1) = (n2k2)