no goals
b o : Ordinal
C : Ordinal → Sort u_2
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNFRec b H0 H o = H o ho (CNFRec b H0 H (o % b ^ log b o))
rw [CNFRec, dif_neg ho]