cases hf''
case refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f' : Quotient inferInstance
hf' : Quotient.choice f = f'
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ f'))
f'' : ν₁ → PropForm ν₂
hf'' : ⟦f''⟧ = f'
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)
case refl.refl
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
hf' : Quotient.choice f = ⟦f''⟧
hv2 :
  v2 ∈
    semVars
      (Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod ⟦p⟧ ⟦f''⟧))
⊢ ∃ a ∈ semVars ⟦p⟧, v2 ∈ semVars (f a)