contradiction
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this✝ :
  ∀ {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 τ
v : V
h : v ∉ L
this : False
⊢ (fun v h => ⋯.elim) v h = τ v
no goals