case a.h.h
f : [0] ⟶ [0]
x✝ : Fin (len [0] + 1)
⊢ ↑(Hom.toOrderHom f) x✝ = ↑(Hom.toOrderHom (𝟙 [0])) x✝
f : [0] ⟶ [0]
⊢ f = 𝟙 [0]
ext : 3
no goals
case a.h.h
f : [0] ⟶ [0]
x✝ : Fin (len [0] + 1)
⊢ ↑(Hom.toOrderHom f) x✝ = ↑(Hom.toOrderHom (𝟙 [0])) x✝
apply @Subsingleton.elim (Fin 1)