Typecheck is sound

theorem typecheck_is_sound (policy : Policy) (env : TypeEnv) (t : CedarType) (request : Request) (entities : Entities) :  InstanceOfWellFormedEnvironment request entities env →  typecheck policy env = .ok t →  (∃ (b : Bool), EvaluatesTo policy.toExpr request entities b):= by  intro h₁ h₂  simp [typecheck] at h₂  cases h₃ : (typeOf (Policy.toExpr policy) [] env).typeOf <;> simp [h₃] at h₂  split at h₂ <;> simp at h₂  rename_i ht  have hc := empty_capabilities_invariant request entities  split_type_of h₃ ; rename_i h₃  have ⟨_, v, h₄, h₅⟩ := type_of_is_sound hc h₁ h₃  simp at h₂  rw [h₂] at ht h₅  have ⟨b, h₆⟩ := instance_of_type_bool_is_bool v t h₅ ht  subst h₆  exists b