Level: Lib Thy Top: 1
Hypotheses:

  1. n :

Conclusion:

n0n1(n) List

Applied Tactic: Unfold `n0n1` 0 THEN Auto
Generated subgoals:

None