theorem Cedar.Thm.partial_eval_well_typed_and {env : Validation.TypeEnv} {a b : Spec.Residual} {ty : Validation.CedarType} {req : Spec.Request} {preq : TPE.PartialRequest} {es : Spec.Entities} {pes : TPE.PartialEntities} : Residual.WellTyped env (TPE.evaluate a preq pes) → Residual.WellTyped env (TPE.evaluate b preq pes) → PEWellTyped env (a.and b ty) (TPE.evaluate (a.and b ty) preq pes) req preq es pes