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