ctx : Context
p : Poly
h :
  (match p with
    | [] => true
    | x => false) =
    true
⊢ denote ctx p = 0
ctx : Context
p : Poly
h : isZero p = true
⊢ denote ctx p = 0
simp [isZero] at h
case h_1
ctx : Context
p✝ : Poly
h : true = true
⊢ denote ctx [] = 0

case h_2
ctx : Context
p p✝ : Poly
x✝ : p = [] → False
h : false = true
⊢ denote ctx p = 0
ctx : Context
p : Poly
h :
  (match p with
    | [] => true
    | x => false) =
    true
⊢ denote ctx p = 0
split at h
no goals
case h_1
ctx : Context
p✝ : Poly
h : true = true
⊢ denote ctx [] = 0
simp
no goals
case h_2
ctx : Context
p p✝ : Poly
x✝ : p = [] → False
h : false = true
⊢ denote ctx p = 0
contradiction