simp at this
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : ⟦Quotient.out (f x)⟧ = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x
ν₁ : Type u_1
ν₂ : Type u_2
φ φ₁ φ₂ : PropFun ν₁
f✝ f₁ : ν₁ → PropFun ν₂
τ✝ : PropAssignment ν₂
v : ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₁ → PropFun ν₂
v2 : ν₂
p : PropForm ν₁
f'' : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
hsat : PropAssignment.subst (fun x => ⟦f'' x⟧) τ ⊨ p
hunsat : ¬PropAssignment.subst (fun x => ⟦f'' x⟧) (PropAssignment.set τ v2 !τ v2) ⊨ p
hf' : ∀ (i : ν₁), PropForm.equivalent (Quotient.out (f i)) (f'' i)
x : ν₁
this : f x = ⟦f'' x⟧
⊢ ⟦f'' x⟧ = f x