Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:. cf:Conf. cf[n] = cf[n + 1]


Applied Tactic: D 0 THENM NatInd 1 THENM UnivCD THENA Auto
Generated subgoals:

1. cf[0] = cf[0 + 1]

2. cf[n] = cf[n + 1]