Partial eval well typed unary App

theorem partial_eval_well_typed_unaryApp {env : TypeEnv} {op : UnaryOp} {expr : Residual} {ty : CedarType} {req : Request} {preq : PartialRequest} {es : Entities} {pes : PartialEntities} :  Residual.WellTyped env (TPE.evaluate expr preq pes) →  PEWellTyped env (Residual.unaryApp op expr ty) (TPE.evaluate (Residual.unaryApp op expr ty) preq pes) req preq es pes:= by  intros h_expr_wt h_wf h_ref h_wt  simp only [TPE.evaluate]  cases h_wt with  | unaryApp h_expr h_op =>    let expr_eval := TPE.evaluate expr preq pes    unfold TPE.apply₁    split    case h_1 => apply Residual.WellTyped.error    case h_2 =>      cases h : expr_eval.asValue with      | some v =>        simp only [someOrError]        split        case h_2 =>          apply Residual.WellTyped.error        case h_1 v ty ox x v₂ heq =>          unfold Spec.apply₁ at heq          split at heq          any_goals            cases h_op            simp only [Except.toOption, Option.some.injEq] at heq            rw [← heq]            exact well_typed_bool          case h_2 =>            simp only [Except.toOption, intOrErr] at heq            rename Int64 => i            cases h₂: i.neg?            . rw [h₂] at heq              simp at heq            . rw [h₂] at heq              simp only [Option.some.injEq] at heq              rw [← heq]              cases h_op              exact well_typed_int          case h_6 =>           contradiction      | none =>        simp only []        split        . cases h_op; exact well_typed_bool        . cases h_op; exact well_typed_bool        . case h_3 =>          apply Residual.WellTyped.unaryApp          exact h_expr_wt          cases h_op          all_goals            first            | apply UnaryResidualWellTyped.not            | apply UnaryResidualWellTyped.neg            | apply UnaryResidualWellTyped.isEmpty            | apply UnaryResidualWellTyped.like            | apply UnaryResidualWellTyped.is            rw [partial_eval_preserves_typeof _ h_expr]            assumption