have : x < k := Nat.succ_lt_succ_iff.mp (lt_of_lt_of_le hx (bv_subtEquiv p))
case hb.succ
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
case hb.succ
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
this : x < k
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)