intros f1_eq_f2 f2_eq_f3 p
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
⊢ liff α f1 f2 → liff α f2 f3 → liff α f1 f3
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_eq_f2 : liff α f1 f2
f2_eq_f3 : liff α f2 f3
p : α → Bool
⊢ p ⊨ f1 ↔ p ⊨ f3