Compile well typed or and

theorem compile_well_typed_or_and  {a : TypedExpr} {b : TypedExpr} {ty : CedarType}  {Γ : TypeEnv} {εnv : SymEnv}  (iha : CompileWellTypedAndWF a εnv)  (ihb : CompileWellTypedAndWF b εnv) :  (CompileWellTypedCondition (.or a b ty) Γ εnv →    CompileWellTyped (.or a b ty) εnv) ∧  (CompileWellTypedCondition (.and a b ty) Γ εnv →    CompileWellTyped (.and a b ty) εnv):= by  constructor  all_goals    intros hcond    have ⟨hεnv, hwt, hwf⟩ := hcond    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    -- By well-typedness, a and b must be booleans    -- So we substitute that fact and simplify    cases hwt; case _ _ hbool_a _ hbool_b =>    simp only [hbool_a, hbool_b] at *; clear hbool_a hbool_b    simp only [TermType.ofType] at *    simp only [      hcomp_a, hcomp_b,      hty_comp_b, hty_comp_a,      CompileWellTyped,      TypedExpr.toExpr,      compile,      compileOr, compileAnd,      Except.bind_ok, ↓reduceIte,    ]    split    · apply Exists.intro; constructor; rfl      simp [TermType.ofType, TypedExpr.typeOf]    · apply Exists.intro; constructor; rfl      apply typeOf_ifSome_option      apply wf_typeOf_ite      any_goals assumption      constructor      apply wf_bool      simp [TermType.ofType, Factory.someOf, TypedExpr.typeOf]    · contradiction