no goals
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h2 next x = next (leRecOn h1 next x)
conv =>
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]