theorem Cedar.Thm.partial_eval_well_typed_ite {env : Validation.TypeEnv} {c t e : Spec.Residual} {ty : Validation.CedarType} {req : Spec.Request} {preq : TPE.PartialRequest} {es : Spec.Entities} {pes : TPE.PartialEntities} : Residual.WellTyped env (TPE.evaluate c preq pes) → Residual.WellTyped env (TPE.evaluate t preq pes) → Residual.WellTyped env (TPE.evaluate e preq pes) → PEWellTyped env (c.ite t e ty) (TPE.evaluate (c.ite t e ty) preq pes) req preq es pes