case h.h
n✝ m n : ℕ
x✝ : Fin n
⊢ ↑(↑(natAdd 0) x✝) = ↑(↑(RelIso.toRelEmbedding (cast (_ : n = 0 + n))) x✝)
n✝ m n : ℕ
⊢ natAdd 0 = RelIso.toRelEmbedding (cast (_ : n = 0 + n))
ext
no goals
case h.h
n✝ m n : ℕ
x✝ : Fin n
⊢ ↑(↑(natAdd 0) x✝) = ↑(↑(RelIso.toRelEmbedding (cast (_ : n = 0 + n))) x✝)
simp