α : Type ?u.95975
β : Type ?u.95978
γ : Type ?u.95981
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
⊢ Eq.mpr (_ : C 0 = C 0) H₁ = H₁
α : Type ?u.95975
β : Type ?u.95978
γ : Type ?u.95981
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
⊢ limitRecOn 0 H₁ H₂ H₃ = H₁
rw [limitRecOn, lt_wf.fix_eq, dif_pos rfl]
no goals
α : Type ?u.95975
β : Type ?u.95978
γ : Type ?u.95981
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
C : Ordinal → Sort u_2
H₁ : C 0
H₂ : (o : Ordinal) → C o → C (succ o)
H₃ : (o : Ordinal) → IsLimit o → ((o' : Ordinal) → o' < o → C o') → C o
⊢ Eq.mpr (_ : C 0 = C 0) H₁ = H₁
rfl