Add inductive relation for level checking

cedar-lean/Cedar/Thm/Validation.lean

@@ -19,6 +19,7 @@ import Cedar.Data
 import Cedar.Validation
 import Cedar.Thm.Validation.Validator
 import Cedar.Thm.Validation.RequestEntityValidation
+import Cedar.Thm.Validation.Levels
 
 /-!
 This file contains the top-level correctness properties for the Cedar validator.

cedar-lean/Cedar/Thm/Validation/Levels.lean

@@ -0,0 +1,17 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.Thm.Validation.Levels.CheckLevel