ext τ
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
⊢ toPropFun (or c1 c2) = toPropFun c1 ⊔ toPropFun c2
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (or c1 c2) ↔ τ ⊨ toPropFun c1 ⊔ toPropFun c2