Wf env implies wf request

theorem wf_env_implies_wf_request  {env : TypeEnv}  (hwf : env.WellFormed) :  EntityType.WellFormed env env.reqty.principal ∧  env.acts.contains env.reqty.action ∧  EntityType.WellFormed env env.reqty.resource ∧  (CedarType.record env.reqty.context).WellFormed env:= by  have ⟨_, hwf_acts, ⟨entry, hwf_act, hwf_princ, hwf_res, hwf_ctx⟩⟩ := hwf  have ⟨_, hwf_acts, _⟩ := hwf_acts  have hwf_act_entry := hwf_acts env.reqty.action entry hwf_act  have ⟨_, _, _, hwf_app_to_princ, hwf_app_to_res, _, hwf_ctx_ty⟩ := hwf_act_entry  and_intros  · apply hwf_app_to_princ    simp only [Membership.mem] at hwf_princ    simp [Set.contains, hwf_princ, Membership.mem]  · simp [ActionSchema.contains, hwf_act]  · apply hwf_app_to_res    simp only [Membership.mem] at hwf_res    simp [Set.contains, hwf_res, Membership.mem]  · simp [hwf_ctx, hwf_ctx_ty]