Level:
Lib
Thy
Top
:
1
Hypotheses:
n :
k :
cf : Conf
m : Atom
m' : Atom
cf[n] = <SKIP, m>
cf[n + k] = <SKIP, m'>
Conclusion:
m = m'
Applied Tactic:
RWH (RevLemmaC `nth_compose`) 7 THENA Auto
Generated subgoals:
1
. m = m'