Theorem: LeanSAT.Model.PropFun.entails.antisymm (LeanSAT/Model/PropFun.lean)

State before:
ν✝ : Type u_1
φ ψ : PropFun ν✝
⊢ entails φ ψ → entails ψ φ → φ = ψ
Tactic:
intro h₁ h₂
State after:
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
⊢ φ = ψ

State before:
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
⊢ φ = ψ
Tactic:
ext τ
State after:
case a
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
τ : PropAssignment ν✝
⊢ τ ⊨ φ ↔ τ ⊨ ψ

State before:
case a
ν✝ : Type u_1
φ ψ : PropFun ν✝
h₁ : entails φ ψ
h₂ : entails ψ φ
τ : PropAssignment ν✝
⊢ τ ⊨ φ ↔ τ ⊨ ψ
Tactic:
exact ⟨entails_ext.mp h₁ τ, entails_ext.mp h₂ τ⟩
State after:
no goals