exact this.symm
case intro.mk.intro.a.e_a.h.h.h
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
f : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
p : PropForm ν₁
f' : ν₁ → PropForm ν₂
x : ν₁
hq : (fun i => Quotient.out (f i)) ≈ f'
this : f x = ⟦f' x⟧
⊢ ⟦f' x⟧ = f x
no goals