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