C : Ordinal → Sort u_2
b : Ordinal
H0 : C 0
H : (o : Ordinal) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ Eq.mpr (_ : C 0 = C 0) H0 = H0
C : Ordinal → Sort u_2
b : Ordinal
H0 : C 0
H : (o : Ordinal) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNFRec b H0 H 0 = H0
rw [CNFRec, dif_pos rfl]
no goals
C : Ordinal → Sort u_2
b : Ordinal
H0 : C 0
H : (o : Ordinal) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ Eq.mpr (_ : C 0 = C 0) H0 = H0
rfl