Opt compile correctness has Attr

theorem Opt.compile.correctness.hasAttr (expr : Expr) (attr : Attr) (εnv : SymEnv) :  Opt.compile (.hasAttr expr attr) εnv = (do    let term ← SymCC.compile (.hasAttr expr attr) εnv    let footprint := footprint (.hasAttr expr attr) εnv    .ok { term, footprint }  ):= by  simp [Opt.compile, SymCC.compile, footprint]  rw [Opt.compile.correctness expr εnv]  cases h₁ : SymCC.compile expr εnv <;> simp  case ok t =>    rw [Opt.compileHasAttr.correctness]    simp only [Opt.CompileResult.mapTerm, bind_assoc, Except.bind_ok]