Opt compile correctness set

theorem Opt.compile.correctness.set (ls : List Expr) (εnv : SymEnv) :  Opt.compile (.set ls) εnv = (do    let term ← SymCC.compile (.set ls) εnv    let footprint := footprint (.set ls) εnv    .ok { term, footprint }  ):= by  simp [Opt.compile, SymCC.compile, footprint]  rw [List.mapM₁_eq_mapM (Opt.compile · εnv), List.mapM₁_eq_mapM (SymCC.compile · εnv)]  rw [List.mapUnion₁_eq_mapUnion (footprint · εnv)]  simp_do_let ls.mapM (Opt.compile · εnv) as hmap₁  <;> simp_do_let ls.mapM (SymCC.compile · εnv) as hmap₂  case error.error e₁ e₂ =>    simp only [Except.error.injEq]    apply both_lists_error_then_errors_same hmap₁ hmap₂    intro x hx    have := List.sizeOf_lt_of_mem hx -- for termination    exact Opt.compile.correctness x εnv  case ok.error ts e =>    exfalso    replace ⟨x, hx, hmap₂⟩ := List.mapM_error_implies_exists_error hmap₂    replace ⟨t, ht, hmap₁⟩ := List.mapM_ok_implies_all_ok hmap₁ x hx    have := List.sizeOf_lt_of_mem hx -- for termination    rw [Opt.compile.correctness] at hmap₁    simp [hmap₂] at hmap₁  case error.ok e ts =>    exfalso    replace ⟨x, hx, hmap₁⟩ := List.mapM_error_implies_exists_error hmap₁    replace ⟨t, ht, hmap₂⟩ := List.mapM_ok_implies_all_ok hmap₂ x hx    have := List.sizeOf_lt_of_mem hx -- for termination    rw [Opt.compile.correctness] at hmap₁    simp [hmap₂] at hmap₁  case ok.ok ts₁ ts₂ =>    rw [Opt.compileSet.correctness]    suffices      SymCC.compileSet (List.map Opt.CompileResult.term ts₁) = SymCC.compileSet ts₂      ∧ ts₁.mapUnion Opt.CompileResult.footprint = ls.mapUnion (footprint · εnv)      by simp [this]    have ⟨h₁, h₂⟩ := both_lists_ok_then_elts_correspond hmap₁ hmap₂ (by      intro x hx      have := List.sizeOf_lt_of_mem hx -- for termination      exact Opt.compile.correctness x εnv    )    subst ts₂ ; simp    apply List.map_eqv_implies_mapUnion_eq (by simp [h₂, List.Equiv.refl])