α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx
      (if ContextInformation.isIdem ctx = true then
        mergeIdem
          (if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx (Expr.toList e))
          else removeNeutrals ctx (Expr.toList e))
      else
        if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx (Expr.toList e))
        else removeNeutrals ctx (Expr.toList e)) =
    eval α ctx e
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx (norm ctx e) = eval α ctx e
simp [norm]
no goals
α : Sort u_1
ctx : Context α
e : Expr
⊢ evalList α ctx
      (if ContextInformation.isIdem ctx = true then
        mergeIdem
          (if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx (Expr.toList e))
          else removeNeutrals ctx (Expr.toList e))
      else
        if ContextInformation.isComm ctx = true then sort (removeNeutrals ctx (Expr.toList e))
        else removeNeutrals ctx (Expr.toList e)) =
    eval α ctx e
cases h₁ : ContextInformation.isIdem ctx <;> cases h₂ : ContextInformation.isComm ctx <;>
simp_all [evalList_removeNeutrals, eval_toList, toList_nonEmpty, evalList_mergeIdem, evalList_sort]