case or p q ihp ihq =>
  exact ⟨ihp b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he, ihq b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he⟩
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.or q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 p = bindq b₂ e₂ 0 p ∧ bindq b₁ e₁ 0 q = bindq b₂ e₂ 0 q
no goals