no goals
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h2 (fun {k} => next) (next x) = leRecOn h1 (fun {k} => next) x
rw [Subsingleton.elim h1 (le_trans (le_succ n) h2), leRecOn_trans (le_succ n) h2, leRecOn_succ']