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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
⊢ toPropFun (all ls) = PropFun.all ↑(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 (all ls) ↔ τ ⊨ PropFun.all ↑(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 (all ls) ↔ τ ⊨ PropFun.all ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
simp [satisfies_iff, Clause.satisfies_iff, LitVar.satisfies_iff,
  all, Array.mem_def]
State after:
no goals