simp [*]
case nil.e_a.h
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
v : V
⊢ passn v ⋯ = τ v
no goals