all_goals simp [*]
case and
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝¹ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝¹
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m a✝¹ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝¹ ∧
    bindq b e m a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝

case or
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝¹ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝¹
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m a✝¹ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝¹ ∧
    bindq b e m a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝

case all
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝

case ex
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝
no goals