ctx : Context
p : Poly
k : Nat
⊢ (match p with
      | [] => some 0
      | [(k, v)] => bif v == fixedVar then some k else none
      | x => none) =
      some k →
    denote ctx p = k
ctx : Context
p : Poly
k : Nat
⊢ isNum? p = some k → denote ctx p = k
simp [isNum?]
case h_1
ctx : Context
k : Nat
p✝ : Poly
⊢ some 0 = some k → denote ctx [] = k

case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
ctx : Context
p : Poly
k : Nat
⊢ (match p with
      | [] => some 0
      | [(k, v)] => bif v == fixedVar then some k else none
      | x => none) =
      some k →
    denote ctx p = k
split
case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
case h_1
ctx : Context
k : Nat
p✝ : Poly
⊢ some 0 = some k → denote ctx [] = k

case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
next => intro h; injection h
case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
case h_2
ctx : Context
k : Nat
p✝ : Poly
k✝ : Nat
v✝ : Var
⊢ (bif v✝ == fixedVar then some k✝ else none) = some k → denote ctx [(k✝, v✝)] = k

case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
next k v => by_cases h : v == fixedVar <;> simp [h]; intros; simp [Var.denote, eq_of_beq h]; assumption
no goals
case h_3
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
next => intros; contradiction
ctx : Context
k : Nat
p✝ : Poly
h : some 0 = some k
⊢ denote ctx [] = k
ctx : Context
k : Nat
p✝ : Poly
⊢ some 0 = some k → denote ctx [] = k
intro h
no goals
ctx : Context
k : Nat
p✝ : Poly
h : some 0 = some k
⊢ denote ctx [] = k
injection h
case inl
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k✝ → k * Var.denote ctx v = k✝
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
⊢ (bif v == fixedVar then some k else none) = some k✝ → denote ctx [(k, v)] = k✝
by_cases h : v == fixedVar <;> simp [h]
case inl
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k * Var.denote ctx v = k✝
case inl
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k✝ → k * Var.denote ctx v = k✝
intros
case inl
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k = k✝
case inl
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k * Var.denote ctx v = k✝
simp [Var.denote, eq_of_beq h]
no goals
case inl
ctx : Context
k✝ : Nat
p✝ : Poly
k : Nat
v : Var
h : (v == fixedVar) = true
a✝ : k = k✝
⊢ k = k✝
assumption
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
a✝ : none = some k
⊢ denote ctx p = k
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
⊢ none = some k → denote ctx p = k
intros
no goals
ctx : Context
p : Poly
k : Nat
p✝ : Poly
x✝¹ : p = [] → False
x✝ : ∀ (k : Nat) (v : Var), p = [(k, v)] → False
a✝ : none = some k
⊢ denote ctx p = k
contradiction