Opt compile correctness andor

theorem Opt.compile.correctness.andor (x₁ x₂ : Expr) (εnv : SymEnv) :  Opt.compile (.and x₁ x₂) εnv = (do    let term ← SymCC.compile (.and x₁ x₂) εnv    let footprint := footprint (.and x₁ x₂) εnv    .ok { term, footprint }  )  ∧  Opt.compile (.or x₁ x₂) εnv = (do    let term ← SymCC.compile (.or x₁ x₂) εnv    let footprint := footprint (.or x₁ x₂) εnv    .ok { term, footprint }  ):= by  constructor  all_goals {    simp [Opt.compile, SymCC.compile, footprint]    rw [Opt.compile.correctness x₁ εnv, Opt.compile.correctness x₂ εnv]    simp [Opt.compileAnd, SymCC.compileAnd, Opt.compileOr, SymCC.compileOr, footprint.ofBranch, EmptyCollection.emptyCollection]    cases h₁ : SymCC.compile x₁ εnv <;> simp only [Except.bind_ok, Except.bind_err]    case ok t₁ =>      cases h₂ : SymCC.compile x₂ εnv <;> simp only [Except.bind_ok, Except.bind_err]      case error e => split <;> simp [*]      case ok t₂ =>        split <;> simp [*]        split <;> simp at *        split <;> simp [*]        first        | rw [Data.Set.union_empty_right (Data.Set.union_wf _ _)]        | rw [Data.Set.union_empty_right (footprint_wf _ _)]  }