induction rem with
| nil => simp [ofFun.aux]; congr; funext v; simp [*]
| cons head tail ih =>
  simp
  cases hhead : τ head <;> (simp; apply ih; intro v h; split <;> simp [*])
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
ht : ∀ (v : V) (h : v ∉ rem), passn v h = τ v
⊢ eval τ (ofFun.aux p rem passn) = p τ
no goals