no goals
I : Type u
α : Type u_3
β : Type u_2
γ : Type u_1
f✝ : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f✝ i
i : I
inst✝ : One γ
f : α → β
x✝ : β
⊢ extend f 1 1 x✝ = OfNat.ofNat 1 x✝
apply ite_self