Theorem: Sat.limplies_unsat (LeanSAT/Sat/Basic.lean)

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f2 f1
⊢ unsatisfiable α f1 → unsatisfiable α f2
Tactic:
intros f1_unsat p p_entails_f2
State after:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f2 f1
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False

State before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : limplies α f2 f1
f1_unsat : unsatisfiable α f1
p : α → Bool
p_entails_f2 : p ⊨ f2
⊢ False
Tactic:
exact f1_unsat p $ h p p_entails_f2
State after:
no goals