unfold ofFun
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun p L hc) = p τ
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 τ