no goals
ctx : Context
m₁ m₂ : Mon
⊢ denote ctx (m₁ ++ m₂) = denote ctx m₁ * denote ctx m₂
match m₁ with
| [] => simp! [Nat.one_mul]
| v :: m₁ => simp! [append_denote ctx m₁ m₂, Nat.mul_assoc]
no goals
ctx : Context
m₁ m₂ : Mon
⊢ denote ctx ([] ++ m₂) = denote ctx [] * denote ctx m₂
simp! [Nat.one_mul]
no goals
ctx : Context
m₁✝ m₂ : Mon
v : Var
m₁ : List Var
⊢ denote ctx (v :: m₁ ++ m₂) = denote ctx (v :: m₁) * denote ctx m₂
simp! [append_denote ctx m₁ m₂, Nat.mul_assoc]