rw [satisfies_mk, PropForm.satisfies_subst, ← satisfies_mk]
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')⟧
⊢ τ ⊨ ⟦PropForm.subst p f'⟧ ↔ 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')⟧
⊢ PropAssignment.subst (fun x => ⟦f' x⟧) τ ⊨ ⟦p⟧ ↔ PropAssignment.subst f τ ⊨ φ