theorem any_filter_imp:  "(∀x. ¬s x ⟹ ¬t x) ⟹  list_ex t (filter s l) =  list_ex (λx. s x) l"
Auto Quickcheck found a counterexample:
  s = {a⇩1}
  t = {}
  x = a⇩1
  l = [a⇩1]
Evaluated terms:
  list_ex t (filter s l) = False
  list_ex s l = True

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
open Classical
theorem any_filter_imp (s t : a -> Bool): (∀ x : a, ¬ (s x) -> ¬ (t x)) -> ∀ l : List a,l.any t <-> (l.filter s).any t :=
  by
  intro hst l
  simp
  induction' l with hd tl ht
  simp
  cases' Classical.em (s hd) with hsh hnsh
  simp
  rw [hsh]
  simp
  rw [ht]
  simp at hnsh
  have hnt : ¬ t hd := by {
    apply hst
    simp
    exact hnsh
  }
  simp
  simp at hnt
  rw [hnt]
  simp
  rw [ht]

theorem any_filter_imp:  "(∀x. ¬s x ⟶ ¬t x) ⟹ ((∃x ∈ (set (filter s l)). t x) = (∃x ∈ (set l). t x))"

datatype 'a normalizable =
  Atom 'a
| And "'a normalizable" "'a normalizable"
| Or "'a normalizable" "'a normalizable"
| Not "'a normalizable"


definition coherent :: "(bool × 'a normalizable) list list list ⇒ bool" where
  "coherent n = ( (n = []) ∨ (list_all (λg. (list_all (λs. ¬(s = []) ∧ (distinct (map (λx. snd x) s))) g) ∨ (g = []) ) n))"

definition makeCoherent :: "(bool × 'a normalizable) list list list ⇒ (bool × 'a normalizable) list list list" where
  "makeCoherent n = map (λx. map remdups (filter (λy. (list_all2 (λa b. snd a = snd b ⟶ fst a = fst b) y y) ∧ ¬(y = [])) x)) n"

theorem coherency: "coherent (makeCoherent n)"

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

def coherent (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  ∀ g : List (List (Bool × normalizable α pred)), g ∈ n ->
  ∀ s : List (Bool × normalizable α pred), s ∈ g ->
  (∀ w : Bool × normalizable α pred,∀ x : Bool × normalizable α pred, w ∈ s ∧ x ∈ s ->
  w.snd == x.snd -> w.fst == x.fst) ∧ s.Nodup

def makeCoherent (n : List (List (List (Bool × normalizable α pred)))) : List (List (List (Bool × normalizable α pred))) :=
  n.map
  (fun x => (x.filter
  (fun y => y.Pairwise
  (fun a b => a.snd = b.snd -> a.fst = b.fst))).map
  (fun y => y.dedup))

theorem coherency : ∀ n : List (List (List (Bool × normalizable α pred))), coherent (makeCoherent n) :=
  by
  intro n g hg s hs
  unfold makeCoherent at hg
  obtain ⟨a, _, ha_transformed_to_g⟩ := List.mem_map.mp hg
  subst ha_transformed_to_g
  constructor
  intros w x hw heqw
  rw [List.mem_map] at hs
  obtain ⟨b, hb_in_filtered_a, hb_eq_s⟩ := hs
  subst hb_eq_s
  rw [List.mem_filter] at hb_in_filtered_a
  obtain ⟨hb_in_a, hb_pw⟩ := hb_in_filtered_a
  have hb_pairwise : b.Pairwise (fun c d => c.snd = d.snd → c.fst = d.fst) := by simpa using hb_pw
  have snd_eq : w.snd = x.snd := by simpa using heqw
  have hp : ∀ c d, c ∈ b ∧ d ∈ b → c.2 = d.2 → c.1 = d.1 := by
    intro c d ⟨hc, hd⟩
    refine List.Pairwise.forall_of_forall ?_ (by simp) hb_pairwise hc hd
    intro x y h1 h2
    exact (h1 (h2.symm)).symm
  obtain ⟨ hw_left, hw_right⟩ := hw
  simp
  apply hp
  constructor
  rw [← List.mem_dedup]
  exact hw_left
  rw [← List.mem_dedup]
  exact hw_right
  rw [beq_iff_eq] at heqw
  exact heqw
  simp [List.nodup_dedup] at hs
  obtain ⟨b, _, hb_eq_s⟩ := hs
  rw [← hb_eq_s]
  exact List.nodup_dedup b

quickcheck[eval="makeCoherent n"]

  nitpick[eval="makeCoherent n""map (λx. map remdups (filter (λy. (list_all2 (λa b. snd a = snd b ⟶ fst a = fst b) y y) ∧ ¬(y = [])) x)) n"]