Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:. (n0) = 1

Applied Tactic: UnivCD THENW Auto THEN RecCaseSplit `exp` THEN Auto
Generated subgoals:

None