theorem Cedar.Thm.instance_of_bool_type_refl {b : Bool} {bty : Validation.BoolType} : Validation.instanceOfBoolType b bty = true → InstanceOfBoolType b bty

theorem Cedar.Thm.instance_of_entity_type_refl {e : Spec.EntityUID} {ety : Spec.EntityType} {env : Validation.TypeEnv} : Validation.instanceOfEntityType e ety env = true → InstanceOfEntityType e ety env

theorem Cedar.Thm.instance_of_ext_type_refl {ext : Spec.Ext} {extty : Validation.ExtType} : Validation.instanceOfExtType ext extty = true → InstanceOfExtType ext extty

@[irreducible]

theorem Cedar.Thm.instance_of_type_refl {v : Spec.Value} {ty : Validation.CedarType} {env : Validation.TypeEnv} : Validation.instanceOfType v ty env = true → InstanceOfType env v ty

theorem Cedar.Thm.instance_of_request_type_refl {request : Spec.Request} {env : Validation.TypeEnv} : Validation.instanceOfRequestType request env = true → InstanceOfRequestType request env

theorem Cedar.Thm.instance_of_schema_refl {entities : Spec.Entities} {env : Validation.TypeEnv} : Validation.instanceOfSchema entities env = Except.ok () → InstanceOfSchema entities env

theorem Cedar.Thm.instance_of_well_formed_env {env : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} : env.validateWellFormed = Except.ok () → Validation.requestMatchesEnvironment env request = true → Validation.entitiesMatchEnvironment env entities = Except.ok () → InstanceOfWellFormedEnvironment request entities env

theorem Cedar.Thm.request_and_entities_validate_implies_instance_of_wf_schema (schema : Validation.Schema) (request : Spec.Request) (entities : Spec.Entities) : schema.validateWellFormed = Except.ok () → Validation.validateRequest schema request = Except.ok () → Validation.validateEntities schema entities = Except.ok () → InstanceOfWellFormedSchema schema request entities