generalize hq : φ.prod (Quotient.choice f) = q
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ (Quotient.prod φ (Quotient.choice f)) ↔
    PropAssignment.subst f τ ⊨ φ
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
q : Quotient (Setoid.prod (setoid ν₁) inferInstance)
hq : Quotient.prod φ (Quotient.choice f) = q
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ q ↔
    PropAssignment.subst f τ ⊨ φ