Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n,k:. cf:Conf. m,m':Atom . cf[n] = <SKIP, m> cf[n + k] = <SKIP, m'> m = m'

Applied Tactic: UnivCD THENA Auto'
Generated subgoals:

1. m = m'