ctx : Context
k : Nat
p : Poly
⊢ denote ctx (bif k == 0 then [] else bif k == 1 then p else mul.go k p) = k * denote ctx p
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (mul k p) = k * denote ctx p
simp
case inl
ctx : Context
k : Nat
p : Poly
h : (k == 0) = true
⊢ 0 = k * denote ctx p

case inr
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (bif k == 0 then [] else bif k == 1 then p else mul.go k p) = k * denote ctx p
by_cases h : k == 0 <;> simp [h]
case inr
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p
case inl
ctx : Context
k : Nat
p : Poly
h : (k == 0) = true
⊢ 0 = k * denote ctx p

case inr
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p
simp [eq_of_beq h]
case inr.inl
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : (k == 1) = true
⊢ denote ctx p = k * denote ctx p

case inr.inr
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p
case inr
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p
by_cases h : k == 1 <;> simp [h]
case inr.inr
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p
case inr.inl
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : (k == 1) = true
⊢ denote ctx p = k * denote ctx p

case inr.inr
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p
simp [eq_of_beq h]
no goals
case inr.inr
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p
induction p with
| nil  => simp
| cons kv m ih => cases kv with | _ k' v => simp [ih]
no goals
case inr.inr.nil
ctx : Context
k : Nat
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k []) = k * denote ctx []
simp
no goals
case inr.inr.cons
ctx : Context
k : Nat
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
kv : Nat × Var
m : List (Nat × Var)
ih : denote ctx (mul.go k m) = k * denote ctx m
⊢ denote ctx (mul.go k (kv :: m)) = k * denote ctx (kv :: m)
cases kv with | _ k' v => simp [ih]
no goals
case inr.inr.cons.mk
ctx : Context
k : Nat
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
m : List (Nat × Var)
ih : denote ctx (mul.go k m) = k * denote ctx m
k' : Nat
v : Var
⊢ denote ctx (mul.go k ((k', v) :: m)) = k * denote ctx ((k', v) :: m)
simp [ih]