Level: Lib Thy Top: 1 1
Hypotheses:

  1. n :

  2. k :

  3. cf : Conf

  4. m : Atom

  5. m' : Atom

  6. cf[n] = <SKIP, m>

  7. cf[n][k] = <SKIP, m'>

Conclusion:

m = m'

Applied Tactic: RWH (HypC 6) 7 THENA Auto
Generated subgoals:

1. m = m'