Compile well typed on wf expr

theorem compile_well_typed_on_wf_expr {Γ : TypeEnv} {εnv : SymEnv} {tx : TypedExpr} :  CompileWellTypedCondition tx Γ εnv →  CompileWellTyped tx εnv:= by  intros h  cases tx  case lit => exact compile_well_typed_lit h  case var => exact compile_well_typed_var h  case ite =>    have ⟨h1, h2, h3⟩ := h.eliminate_ite    apply compile_well_typed_ite    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    any_goals assumption  case and =>    have ⟨ha, hb⟩ := h.eliminate_or_and ?_    apply (compile_well_typed_or_and ?_ ?_).right    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    any_goals assumption    any_goals simp  case or =>    have ⟨ha, hb⟩ := h.eliminate_or_and ?_    apply (compile_well_typed_or_and ?_ ?_).left    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    any_goals assumption    any_goals simp  case unaryApp =>    have hcond := h.eliminate_unaryApp    apply compile_well_typed_unaryApp    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    all_goals assumption  case binaryApp =>    have ⟨ha, hb⟩ := h.eliminate_binaryApp    apply compile_well_typed_binaryApp    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    any_goals assumption  case getAttr =>    have hcond := h.eliminate_getAttr    apply compile_well_typed_getAttr    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    all_goals assumption  case hasAttr =>    have hcond := h.eliminate_hasAttr    apply compile_well_typed_hasAttr    any_goals apply CompileWellTyped.add_wf    any_goals apply compile_well_typed_on_wf_expr    all_goals assumption  case set =>    have hcond := h.eliminate_set    apply compile_well_typed_set    · intros x hx      apply CompileWellTyped.add_wf      apply compile_well_typed_on_wf_expr (hcond x hx)      apply hcond      assumption    assumption  case record =>    have hcond := h.eliminate_record    apply compile_well_typed_record    · intros a x hx      apply CompileWellTyped.add_wf      apply compile_well_typed_on_wf_expr (hcond a x hx)      apply hcond      assumption    assumption  case call =>    have hcond := h.eliminate_call    apply compile_well_typed_call    · intros x hx      apply CompileWellTyped.add_wf      apply compile_well_typed_on_wf_expr (hcond x hx)      apply hcond      assumption    assumption  decreasing_by    repeat case _ =>      simp [*]; omega    -- Set    · simp [*]      have h := List.sizeOf_lt_of_mem hx      omega    -- Record    · simp [*]      have h := List.sizeOf_snd_lt_sizeOf_list hx      simp at h      omega    -- Call    · simp [*]      have h := List.sizeOf_lt_of_mem hx      omega