case h
n✝ m✝ p m n : ℕ
i : Fin n
⊢ ↑(↑(castAdd p) (↑(natAdd m) i)) = ↑(↑(cast (_ : m + (n + p) = m + n + p)) (↑(natAdd m) (↑(castAdd p) i)))
n✝ m✝ p m n : ℕ
i : Fin n
⊢ ↑(castAdd p) (↑(natAdd m) i) = ↑(cast (_ : m + (n + p) = m + n + p)) (↑(natAdd m) (↑(castAdd p) i))
ext
no goals
case h
n✝ m✝ p m n : ℕ
i : Fin n
⊢ ↑(↑(castAdd p) (↑(natAdd m) i)) = ↑(↑(cast (_ : m + (n + p) = m + n + p)) (↑(natAdd m) (↑(castAdd p) i)))
simp