Sound bound analysis produces sound slices

theorem sound_bound_analysis_produces_sound_slices (ba : BoundAnalysis) (request : Request) (entities : Entities) (policies : Policies) :  IsSoundBoundAnalysis ba →  IsSoundPolicySlice request entities (ba.slice request entities policies) policies:= by  unfold IsSoundBoundAnalysis  unfold IsSoundPolicySlice  intro h₁  unfold BoundAnalysis.slice  apply And.intro  case left =>    intro p _    simp_all only [List.mem_filter]  case right =>    intro policy    specialize h₁ policy    intro h₂ h₃    rw [List.mem_filter] at h₃    simp only [h₂, true_and, Bool.not_eq_true] at h₃    by_contra h₄    simp only [Bool.not_eq_true, not_and, Bool.not_eq_false] at h₄    unfold IsSoundPolicyBound at h₁    specialize h₁ request entities    have ⟨h₅, h₆⟩ := h₁; clear h₁    simp only [h₃, Bool.false_eq_true, imp_false, Bool.not_eq_true] at h₅ h₆    specialize h₄ h₅    simp only [h₄, Bool.true_eq_false] at h₆