Enforce Pair Compiled Policy eqv enforce ok

theorem enforcePairCompiledPolicy_eqv_enforce_ok {p₁ p₂ wp₁ wp₂ : Policy} {cp₁ cp₂ : CompiledPolicy} {Γ : Validation.TypeEnv} :  CompiledPolicy.compile p₁ Γ = .ok cp₁ →  CompiledPolicy.compile p₂ Γ = .ok cp₂ →  wellTypedPolicy p₁ Γ = .ok wp₁ →  wellTypedPolicy p₂ Γ = .ok wp₂ →  enforce [wp₁.toExpr, wp₂.toExpr] (SymEnv.ofTypeEnv Γ) = enforcePairCompiledPolicy cp₁ cp₂:= by  simp [enforce, enforcePairCompiledPolicy]  intro h₀ h₁ h₂ h₃  simp [    cp_compile_produces_the_right_env h₀,    cp_compile_produces_the_right_env h₁,    cp_compile_produces_the_right_footprint h₀,    cp_compile_produces_the_right_footprint h₁,    cp_compile_produces_the_right_acyclicity h₀,    cp_compile_produces_the_right_acyclicity h₁,    cp_compile_produces_the_right_policy h₀ h₂,    cp_compile_produces_the_right_policy h₁ h₃,  ]  have h_split : [wp₁.toExpr, wp₂.toExpr] = [wp₁.toExpr] ++ [wp₂.toExpr] := by simp  rw [h_split, footprints_append, footprints_singleton, footprints_singleton]  simp [Data.Set.make_make_eqv, List.Equiv, List.subset_def]  constructor  · intro t₁ h₁    cases h₁ <;> rename_i h₁    · replace ⟨t₂, h₁, htemp⟩ := h₁ ; subst t₁      simp only [List.cons_append, List.nil_append, Data.Set.mem_elts_iff_mem_set,        Data.Set.mem_map] at *      change t₂ ∈ _ ∪ _ at h₁      rw [Data.Set.mem_union] at h₁      cases h₁ <;> rename_i h₁      case' inl => left      case' inr => right ; left      all_goals exists t₂    · right ; right      simp [*]  · intro t₁ h₁    cases h₁ <;> rename_i h₁ <;> try (cases h₁ <;> rename_i h₁)    case right.inr.inr => right ; exact h₁    case' right.inl | right.inr.inl =>      left      simp [Data.Set.mem_elts_iff_mem_set, Data.Set.mem_map] at h₁      replace ⟨t₂, h₁, htemp⟩ := h₁ ; subst t₁      exists t₂      simp [Data.Set.mem_elts_iff_mem_set, HAppend.hAppend]      change t₂ ∈ _ ∪ _      rw [Data.Set.mem_union]    case' right.inl => left    case' right.inr.inl => right    all_goals exact h₁