Compile ok implies compile well typed binary App

theorem compile_ok_implies_compile_well_typed_binaryApp  {op : BinaryOp} {a : TypedExpr} {b : TypedExpr} {ty : CedarType}  {Γ : TypeEnv} {εnv : SymEnv}  (iha : CompileWellTypedAndWF a εnv)  (ihb : CompileWellTypedAndWF b εnv)  (hcond : CompileWellTypedCondition (.binaryApp op a b ty) Γ εnv)  (hok : ∃ t : Term,    compile (TypedExpr.toExpr (.binaryApp op a b ty)) εnv = .ok t) :  CompileWellTyped (.binaryApp op a b ty) εnv:= by  have ⟨hεnv, hwt_binary, ⟨hwf_εnv, hrefs_binary⟩⟩ := hcond  have ⟨hwf_req, hwf_ent⟩ := hwf_εnv  have ⟨tcomp_a, hcomp_a, hty_comp_a, hwf_comp_a⟩ := iha  have ⟨tcomp_b, hcomp_b, hty_comp_b, hwf_comp_b⟩ := ihb  have ⟨hwf_get_comp_a, hty_get_comp_a⟩ := wf_option_get hwf_comp_a hty_comp_a  have ⟨hwf_get_comp_b, hty_get_comp_b⟩ := wf_option_get hwf_comp_b hty_comp_b  have ⟨t, hok⟩ := hok  have htypes := compile_binaryApp_wf_types    hwf_ent hcomp_a hcomp_b hwf_get_comp_a hwf_get_comp_b hok  cases hwt_binary with | binaryApp _ _ hopwt =>  cases hopwt  -- Simplify and resolve most goals  all_goals    simp only [      CompileWellTyped, TypedExpr.toExpr, TypedExpr.typeOf, TermType.ofType,    ]    simp only [TypedExpr.toExpr] at hok    simp only [exists_and_left] at htypes    simp only [hok, Except.ok.injEq, exists_eq_left', htypes]  -- Special case for `getTag`  case getTag _ ety tags htag hty_a hty_b _ _ =>    have ⟨ety2, hty_get_comp_a2, τs, hτag, hτag_ty⟩ := htypes    rw [← ofType_eq_ofType_liftBool]    have ⟨τs2, hτag2, hτag_ty2⟩ := ofEnv_preserves_tags htag    have heq_ety : ety = ety2 := by      simp [hty_get_comp_a, hty_a, TermType.ofType] at hty_get_comp_a2      assumption    have hτs : τs = τs2 := by      simp [← hεnv, heq_ety, hτag] at hτag2      assumption    simp [← hτag_ty2, hτag_ty, hτs]