cases h1
case a.mp.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1 ∨ l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ (∃ 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 ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l