simp[bv]
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (func f v).bv
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv