Compile binary App wf types

theorem compile_binaryApp_wf_types  {op : BinaryOp} {a : TypedExpr} {b : TypedExpr} {ty : CedarType}  {t : Term} {tcomp_a : Term} {tcomp_b : Term}  {εnv : SymEnv}  (hwf_ent : εnv.entities.WellFormed)  (hok_a : compile a.toExpr εnv = Except.ok tcomp_a)  (hok_b : compile b.toExpr εnv = Except.ok tcomp_b)  (hwf_get_comp_a : Term.WellFormed εnv.entities (Factory.option.get tcomp_a))  (hwf_get_comp_b : Term.WellFormed εnv.entities (Factory.option.get tcomp_b))  (hok : compile (TypedExpr.toExpr (.binaryApp op a b ty)) εnv = .ok t) :  match op with    | .add | .sub | .mul => t.typeOf = .option (.bitvec 64)    | .getTag            =>      ∃ ety τs,        (Factory.option.get tcomp_a).typeOf = .entity ety ∧        εnv.entities.tags ety = some (some τs) ∧        t.typeOf = τs.vals.outType.option    | _                  => t.typeOf = .option .bool:= by  simp only [TypedExpr.toExpr, compile, hok_a, hok_b, Except.bind_ok] at hok  simp_do_let    (compileApp₂ op      (Factory.option.get tcomp_a)      (Factory.option.get tcomp_b)      εnv.entities)    at hok  simp only [Except.ok.injEq] at hok  case ok tcomp_app hcomp_app =>    have h := (compileApp₂_wf_types      hwf_ent      hwf_get_comp_a      hwf_get_comp_b      hcomp_app    ).right    -- tcomp_app and t should have the same type    have heqty : t.typeOf = tcomp_app.typeOf    := by      simp only [← hok]      cases op      any_goals        simp only [h]        apply typeOf_ifSome_option        apply typeOf_ifSome_option        assumption      -- Special case for getTag      case getTag =>        have ⟨_, _, _, _, h⟩ := h        simp only [h]        apply typeOf_ifSome_option        apply typeOf_ifSome_option        assumption    cases op    any_goals      simp only [exists_and_left] at h      simp [h, heqty]