unfold subst at hv2
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 : v2 ∈ semVars (subst φ f)
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
v2 : ν₂
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)))
⊢ v2 ∈ Finset.biUnion (semVars φ) fun v1 => semVars (f v1)