Theorem: Sat.liff.symm (LeanSAT/Sat/Basic.lean)

State before:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 → liff α f2 f1
Tactic:
intros h p
State after:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 ↔ p ⊨ f1

State before:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 ↔ p ⊨ f1
Tactic:
rw [h p]
State after:
no goals