v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
⊢ False
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
⊢ reify v (and f₁ f₂) (a ∨ b)
refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₁
⊢ False

case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₂
⊢ False
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
⊢ False
rcases List.mem_append.1 h with h | h
no goals
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₁
⊢ False
exact hn $ Or.inl $ h₁.1 fun Hc ↦ hn' $ Hc.1 _ h
no goals
case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₂
⊢ False
exact hn $ Or.inr $ h₂.1 fun Hc ↦ hn' $ Hc.1 _ h