no goals
n✝ m n : ℕ
C : Fin (n + 1) → Sort u_1
H0 : C 0
Hs : (i : Fin n) → C (succ i)
i : ℕ
h : i + 1 < n + 1
⊢ cases H0 Hs { val := Nat.succ i, isLt := h } = Hs { val := i, isLt := (_ : i < n) }
cases i <;> rfl