rcases hq with ⟨rfl,hq⟩
case intro.mk
ν₁ : Type u_1
ν₂ : Type u_2
φ✝ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
φ : PropFun ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : φ = ⟦p⟧ ∧ Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ
case intro.mk.intro
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
hq : Quotient.choice f = ⟦f'⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ ⟦p⟧