Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
m:Atom
.
n:
. <SKIP, m>[n] = <SKIP, m>
Applied Tactic:
UnivCD THENM NatInd 2 THENM RecCaseSplit `nth` THEN Auto
Generated subgoals:
None
m:Atom 
. n:
. <SKIP, m>[n] = <SKIP, m> m:Atom . n:. <SKIP, m>[n] = <SKIP, m>