Opt compile correctness binary App

theorem Opt.compile.correctness.binaryApp (op : BinaryOp) (x₁ x₂ : Expr) (εnv : SymEnv) :  Opt.compile (.binaryApp op x₁ x₂) εnv = (do    let term ← SymCC.compile (.binaryApp op x₁ x₂) εnv    let footprint := footprint (.binaryApp op x₁ x₂) εnv    .ok { term, footprint }  ):= by  simp [Opt.compile, SymCC.compile, footprint]  rw [Opt.compile.correctness x₁ εnv, Opt.compile.correctness x₂ εnv]  cases h₁ : SymCC.compile x₁ εnv <;> simp  case ok t₁ =>    cases h₂ : SymCC.compile x₂ εnv <;> simp    case ok t₂ =>      rw [Opt.compileApp₂.correctness op]      simp [Opt.CompileResult.mapTerm]      cases h : SymCC.compileApp₂ op (Factory.option.get t₁) (Factory.option.get t₂) εnv.entities <;> simp      case ok t =>        rw [Opt.directFootprint.correctness (t := Factory.ifSome t₁ (Factory.ifSome t₂ t)) (εnv := εnv) (x := .binaryApp op x₁ x₂)]        · conv => rhs ; rw [Data.Set.union_assoc, Data.Set.union_comm]        · -- here we have to show that the `t` and `x` arguments we chose for `Opt.directFootprint.correctness` in the `rw` above correspond to each other correctly          simp [SymCC.compile, h₁, h₂, h]