refine ⟨l,?_⟩
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l