Theorem: LeanSAT.Cnf.toPropFun_any (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
⊢ toPropFun (any ls) = PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
ext τ
State after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (any ls) ↔ τ ⊨ PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))

State before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (any ls) ↔ τ ⊨ PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
simp [any, toPropFun, Clause.toPropFun]
State after:
no goals