rcases q.exists_rep with ⟨⟨p, f'⟩, rfl⟩
ν₁ : 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 τ ⊨ φ
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.prod φ (Quotient.choice f) = ⟦(p, f')⟧
⊢ τ ⊨
      Quotient.lift
        (fun x =>
          match x with
          | (p, f) => ⟦PropForm.subst p f⟧)
        ⋯ ⟦(p, f')⟧ ↔
    PropAssignment.subst f τ ⊨ φ