α : Type ?u.349670
β : Type ?u.349673
γ : Type ?u.349676
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o₁ : Ordinal
f : (a : Ordinal) → a < o₁ → Ordinal
⊢ blsub o₁ f = blsub o₁ fun a h => f a (_ : a < o₁)
α : Type ?u.349670
β : Type ?u.349673
γ : Type ?u.349676
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o₁ o₂ : Ordinal
f : (a : Ordinal) → a < o₁ → Ordinal
ho : o₁ = o₂
⊢ blsub o₁ f = blsub o₂ fun a h => f a (_ : a < o₁)
subst ho
no goals
α : Type ?u.349670
β : Type ?u.349673
γ : Type ?u.349676
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o₁ : Ordinal
f : (a : Ordinal) → a < o₁ → Ordinal
⊢ blsub o₁ f = blsub o₁ fun a h => f a (_ : a < o₁)
rfl