Enforce Compiled Policy eqv enforce ok

theorem enforceCompiledPolicy_eqv_enforce_ok {p wp : Policy} {cp : CompiledPolicy} {Γ : Validation.TypeEnv} :  CompiledPolicy.compile p Γ = .ok cp →  wellTypedPolicy p Γ = .ok wp →  enforce [wp.toExpr] (SymEnv.ofTypeEnv Γ) = enforceCompiledPolicy cp:= by  simp [enforce, enforceCompiledPolicy]  intro h₀ h₁  simp [    cp_compile_produces_the_right_env h₀,    cp_compile_produces_the_right_footprint h₀,    cp_compile_produces_the_right_acyclicity h₀,    cp_compile_produces_the_right_policy h₀ h₁,  ]  simp [footprints]  simp [Data.Set.make_make_eqv, List.Equiv, List.subset_def]  constructor  · intro t h₂    cases h₂    · left      rename_i h₂      replace ⟨t', h₂, ht⟩ := h₂ ; subst t ; rename Term => t      rw [Data.Set.mem_elts_iff_mem_set] at *      rw [List.mem_mapUnion_iff_mem_exists] at h₂      replace ⟨s, hs, h₂⟩ := h₂      simp at hs ; subst s      simp [Data.Set.mem_map]      exists t    · right      rename_i h₂      replace ⟨s, hs, t', ht', h₂⟩ := h₂ ; subst t ; rename Term => t      simp [Data.Set.mem_elts_iff_mem_set, List.mem_mapUnion_iff_mem_exists] at *      exists s      simp [hs]      exists t  · intro t h₂    cases h₂    · left      rename_i h₂      simp [Data.Set.mem_elts_iff_mem_set, Data.Set.mem_map] at h₂      replace ⟨t', ht', h₂⟩ := h₂ ; subst t ; rename Term => t      exists t      simp [Data.Set.mem_elts_iff_mem_set, List.mem_mapUnion_iff_mem_exists]      exact ht'    · right      rename_i h₂      replace ⟨s, hs, t', ht', h₂⟩ := h₂ ; subst t ; rename Term => t      exists s      rw [Data.Set.mem_elts_iff_mem_set] at *      simp [List.mem_mapUnion_iff_mem_exists, hs]      exists t      simp [Data.Set.mem_elts_iff_mem_set, List.mem_mapUnion_iff_mem_exists, ht']