suffices ∀ {rem passn},
  (∀ v h, passn v h = τ v ) →
  eval τ (ofFun.aux p rem passn) = p τ
  from this (fun v h => by have := h (hc v); contradiction)
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun.aux p L fun v h => ⋯.elim) = p τ
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ