no goals
ctx : Context
p : Poly
⊢ denote ctx (fuse p) = denote ctx p
match p with
| [] => rfl
| (k, v) :: p =>
  have ih := denote_fuse ctx p
  simp
  split
  case _ h => simp [← ih, h]
  case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
no goals
ctx : Context
p : Poly
⊢ denote ctx (fuse []) = denote ctx []
rfl
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
⊢ denote ctx (fuse ((k, v) :: p)) = denote ctx ((k, v) :: p)
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx (fuse ((k, v) :: p)) = denote ctx ((k, v) :: p)
have ih := denote_fuse ctx p
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
⊢ denote ctx
      (match fuse p with
      | [] => [(k, v)]
      | (k', v') :: p' => bif v == v' then (k + k', v) :: p' else (k, v) :: (k', v') :: p') =
    denote ctx p + k * Var.denote ctx v
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
⊢ denote ctx (fuse ((k, v) :: p)) = denote ctx ((k, v) :: p)
simp
case h_1
ctx : Context
p✝¹ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝ : Poly
heq✝ : fuse p = []
⊢ denote ctx [(k, v)] = denote ctx p + k * Var.denote ctx v

case h_2
ctx : Context
p✝² : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝¹ : Poly
k✝ : Nat
v✝ : Var
p✝ : List (Nat × Var)
heq✝ : fuse p = (k✝, v✝) :: p✝
⊢ denote ctx (bif v == v✝ then (k + k✝, v) :: p✝ else (k, v) :: (k✝, v✝) :: p✝) = denote ctx p + k * Var.denote ctx v
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
⊢ denote ctx
      (match fuse p with
      | [] => [(k, v)]
      | (k', v') :: p' => bif v == v' then (k + k', v) :: p' else (k, v) :: (k', v') :: p') =
    denote ctx p + k * Var.denote ctx v
split
case h_2
ctx : Context
p✝² : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝¹ : Poly
k✝ : Nat
v✝ : Var
p✝ : List (Nat × Var)
heq✝ : fuse p = (k✝, v✝) :: p✝
⊢ denote ctx (bif v == v✝ then (k + k✝, v) :: p✝ else (k, v) :: (k✝, v✝) :: p✝) = denote ctx p + k * Var.denote ctx v
case h_1
ctx : Context
p✝¹ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝ : Poly
heq✝ : fuse p = []
⊢ denote ctx [(k, v)] = denote ctx p + k * Var.denote ctx v

case h_2
ctx : Context
p✝² : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝¹ : Poly
k✝ : Nat
v✝ : Var
p✝ : List (Nat × Var)
heq✝ : fuse p = (k✝, v✝) :: p✝
⊢ denote ctx (bif v == v✝ then (k + k✝, v) :: p✝ else (k, v) :: (k✝, v✝) :: p✝) = denote ctx p + k * Var.denote ctx v
case _ h => simp [← ih, h]
no goals
case h_2
ctx : Context
p✝² : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝¹ : Poly
k✝ : Nat
v✝ : Var
p✝ : List (Nat × Var)
heq✝ : fuse p = (k✝, v✝) :: p✝
⊢ denote ctx (bif v == v✝ then (k + k✝, v) :: p✝ else (k, v) :: (k✝, v✝) :: p✝) = denote ctx p + k * Var.denote ctx v
case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
no goals
ctx : Context
p✝¹ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝ : Poly
h : fuse p = []
⊢ denote ctx [(k, v)] = denote ctx p + k * Var.denote ctx v
simp [← ih, h]
case inl
ctx : Context
p✝¹ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝ : Poly
k' : Nat
v' : Var
p' : List (Nat × Var)
h : fuse p = (k', v') :: p'
he : (v == v') = true
⊢ denote ctx p' + (k * Var.denote ctx v + k' * Var.denote ctx v) =
    denote ctx p' + (k * Var.denote ctx v + k' * Var.denote ctx v')
ctx : Context
p✝¹ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝ : Poly
k' : Nat
v' : Var
p' : List (Nat × Var)
h : fuse p = (k', v') :: p'
⊢ denote ctx (bif v == v' then (k + k', v) :: p' else (k, v) :: (k', v') :: p') = denote ctx p + k * Var.denote ctx v
by_cases he : v == v' <;> simp [he, ← ih, h]
no goals
case inl
ctx : Context
p✝¹ : Poly
k : Nat
v : Var
p : List (Nat × Var)
ih : denote ctx (fuse p) = denote ctx p
p✝ : Poly
k' : Nat
v' : Var
p' : List (Nat × Var)
h : fuse p = (k', v') :: p'
he : (v == v') = true
⊢ denote ctx p' + (k * Var.denote ctx v + k' * Var.denote ctx v) =
    denote ctx p' + (k * Var.denote ctx v + k' * Var.denote ctx v')
rw [eq_of_beq he]