Opt compile correctness call

theorem Opt.compile.correctness.call (xfn : ExtFun) (args : List Expr) (εnv : SymEnv) :  Opt.compile (.call xfn args) εnv = (do    let term ← SymCC.compile (.call xfn args) εnv    let footprint := footprint (.call xfn args) ε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 args.mapM (Opt.compile · εnv) as hmap₁  <;> simp_do_let args.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 hterm := 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.compileCall.correctness]    · suffices        SymCC.compileCall xfn (List.map Opt.CompileResult.term ts₁) = SymCC.compileCall xfn ts₂        ∧ ts₁.mapUnion Opt.CompileResult.footprint = args.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])    case hwf =>      intro res hres      have ⟨arg, harg, h₁⟩ := List.mapM_ok_implies_all_from_ok hmap₁ res hres      exact Opt.compile_footprint_wf h₁