Enforce Pair Compiled Policy Set eqv enforce ok

theorem enforcePairCompiledPolicySet_eqv_enforce_ok {ps₁ ps₂ wps₁ wps₂ : Policies} {cpset₁ cpset₂ : CompiledPolicySet} {Γ : Validation.TypeEnv} :  CompiledPolicySet.compile ps₁ Γ = .ok cpset₁ →  CompiledPolicySet.compile ps₂ Γ = .ok cpset₂ →  wellTypedPolicies ps₁ Γ = .ok wps₁ →  wellTypedPolicies ps₂ Γ = .ok wps₂ →  enforce (wps₁.map Policy.toExpr ++ wps₂.map Policy.toExpr) (SymEnv.ofTypeEnv Γ) = enforcePairCompiledPolicySet cpset₁ cpset₂:= by  simp [enforce, enforcePairCompiledPolicySet]  intro hcpset₁ hcpset₂ hwps₁ hwps₂  simp [    cpset_compile_produces_the_right_env hcpset₁,    cpset_compile_produces_the_right_env hcpset₂,    cpset_compile_produces_the_right_footprint hcpset₁,    cpset_compile_produces_the_right_footprint hcpset₂,    cpset_compile_produces_the_right_acyclicity hcpset₁,    cpset_compile_produces_the_right_acyclicity hcpset₂,    cpset_compile_produces_the_right_policies hcpset₁ hwps₁,    cpset_compile_produces_the_right_policies hcpset₂ hwps₂,  ]  simp [footprints_append]  rw [Data.Set.make_make_eqv]  simp [List.Equiv, List.subset_def]  constructor  · intro t₁ h₁    cases h₁ <;> rename_i h₁    · replace ⟨t₂, h₁, htemp⟩ := h₁ ; subst t₁      simp only [Data.Set.mem_elts_iff_mem_set, Data.Set.mem_map] at *      simp only [footprints, List.mapUnion_map]      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 {        simp only [footprints, List.mapUnion_map] at h₁        rw [List.mem_mapUnion_iff_mem_exists] at h₁        replace ⟨x, h₁, h₂⟩ := h₁        exists t₂        simp only [List.mem_mapUnion_iff_mem_exists, Function.comp_apply, and_true]        exists x      }    · 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₁      simp [mem_footprints_iff] at h₁      replace ⟨x, ⟨p, hp, htemp⟩, h₁⟩ := h₁ ; subst x      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 {      simp [mem_footprints_iff]      exists p.toExpr      apply And.intro _ h₁      exists p    }