Theorem: LeanSAT.Model.PropFun.biImpl_eq_impls (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
φ ψ : PropFun ν
⊢ biImpl φ ψ = (φ ⇨ ψ) ⊓ (ψ ⇨ φ)
Tactic:
ext τ
State after:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ψ ↔ τ ⊨ (φ ⇨ ψ) ⊓ (ψ ⇨ φ)

State before:
case a
ν : Type u_1
φ ψ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ biImpl φ ψ ↔ τ ⊨ (φ ⇨ ψ) ⊓ (ψ ⇨ φ)
Tactic:
aesop
State after:
no goals