Opt compile correctness record

theorem Opt.compile.correctness.record (m : List (Attr × Expr)) (εnv : SymEnv) :  Opt.compile (.record m) εnv = (do    let term ← SymCC.compile (.record m) εnv    let footprint := footprint (.record m) εnv    .ok { term, footprint }  ):= by  simp [Opt.compile, SymCC.compile, footprint]  simp only [List.mapM₂_eq_mapM (λ x => do Except.ok (x.fst, ← Opt.compile x.snd εnv)) m]  simp only [List.mapM₂_eq_mapM (λ x => do Except.ok (x.fst, ← SymCC.compile x.snd εnv)) m]  rw [List.mapUnion₂_eq_mapUnion (λ x => footprint x.snd εnv)]  simp_do_let m.mapM (m := SymCC.Result) _ as hmap₁  <;> simp_do_let m.mapM (m := SymCC.Result) _ as hmap₂  case error.error e₁ e₂ =>    simp only [Except.error.injEq]    apply both_lists_pairs_error_then_errors_same hmap₁ hmap₂    intro pair hpair    have := List.sizeOf_lt_of_mem hpair -- for termination    have : sizeOf pair.snd < sizeOf pair := by simp [sizeOf, Prod._sizeOf_1] ; omega    exact Opt.compile.correctness pair.snd ε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    have : sizeOf x.snd < sizeOf x := by simp [sizeOf, Prod._sizeOf_1] ; omega    rw [Opt.compile.correctness] at hmap₁    simp [do_error] 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    have : sizeOf x.snd < sizeOf x := by simp [sizeOf, Prod._sizeOf_1] ; omega    rw [Opt.compile.correctness] at hmap₁    simp [do_error] at hmap₁    simp [hmap₁] at hmap₂  case ok.ok ts₁ ts₂ =>    rw [Opt.compileRecord.correctness]    simp only [Except.ok.injEq, Opt.CompileResult.mk.injEq]    have ⟨h₁, h₂⟩ := both_lists_pairs_ok_then_elts_correspond hmap₁ hmap₂ (by      intro pair hpair      have := List.sizeOf_lt_of_mem hpair -- for termination      have : sizeOf pair.snd < sizeOf pair := by simp [sizeOf, Prod._sizeOf_1] ; omega      exact Opt.compile.correctness pair.snd εnv    )    subst ts₂ ; simp    apply List.map_eqv_implies_mapUnion_eq (by simp [h₂, List.Equiv.refl])