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