From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From VLSM.Lib Require Import Preamble ListExtras StdppExtras StdppListSet.

Utility: List Set Definitions and Results

Definition set_eq {A} (s1 s2 : set A) : Prop :=
  s1 ⊆ s2 /\ s2 ⊆ s1.

By declaring set_eq an Equivalence relation, we enable rewriting with it using the rewrite tactic. See the Coq reference manual for details: https://coq.inria.fr/refman/addendum/generalized-rewriting.html (section "Declaring rewrite relations", subsection "First class setoids and morphisms").

#[export] Instance Equivalence_set_eq {A : Type} : Equivalence (@set_eq A).A: Type
Equivalence set_eq
Proof.A: Type
Equivalence set_eq by firstorder. Qed.

#[export] Instance set_eq_dec `{EqDecision A} : RelDecision (@set_eq A).A: Type
EqDecision0: EqDecision A
RelDecision set_eq
Proof.A: Type
EqDecision0: EqDecision A
RelDecision set_eq
  by intros s1 s2; typeclasses eauto.
Qed.

Lemma set_eq_extract_forall
  {A : Type}
  (l1 l2 : set A)
  : set_eq l1 l2 <-> forall a, (a ∈ l1 <-> a ∈ l2).A: Type
l1, l2: set A
set_eq l1 l2 ↔ (∀ a : A, a ∈ l1 ↔ a ∈ l2)
Proof.A: Type
l1, l2: set A
set_eq l1 l2 ↔ (∀ a : A, a ∈ l1 ↔ a ∈ l2)
  by unfold set_eq; firstorder.
Qed.

Lemma set_eq_fin_set `{FinSet A Cm} (s1 s2 : Cm) :
  s1 ≡ s2 <-> set_eq (elements s1) (elements s2).A, Cm: Type
H: ElemOf A Cm
H0: Empty Cm
H1: Singleton A Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements A Cm
EqDecision0: EqDecision A
H6: FinSet A Cm
s1, s2: Cm
s1 ≡ s2 ↔ set_eq (elements s1) (elements s2)
Proof.A, Cm: Type
H: ElemOf A Cm
H0: Empty Cm
H1: Singleton A Cm
H2: Union Cm
H3: Intersection Cm
H4: Difference Cm
H5: Elements A Cm
EqDecision0: EqDecision A
H6: FinSet A Cm
s1, s2: Cm
s1 ≡ s2 ↔ set_eq (elements s1) (elements s2)
  by rewrite set_eq_extract_forall, set_equiv; setoid_rewrite elem_of_elements.
Qed.

Lemma set_eq_proj1 {A} : forall (s1 s2 : set A),
  set_eq s1 s2 ->
  s1 ⊆ s2.A: Type
∀ s1 s2 : set A, set_eq s1 s2 → s1 ⊆ s2
Proof.A: Type
∀ s1 s2 : set A, set_eq s1 s2 → s1 ⊆ s2
  by intros s1 s2 [].
Qed.

Lemma set_eq_proj2 {A} : forall (s1 s2 : set A),
  set_eq s1 s2 ->
  s2 ⊆ s1.A: Type
∀ s1 s2 : set A, set_eq s1 s2 → s2 ⊆ s1
Proof.A: Type
∀ s1 s2 : set A, set_eq s1 s2 → s2 ⊆ s1
  by intros s1 s2 [].
Qed.

Lemma set_eq_empty_iff
  {A}
  : forall (l : list A),
    set_eq l [] <-> l = [].A: Type
∀ l : list A, set_eq l [] ↔ l = []
Proof.A: Type
∀ l : list A, set_eq l [] ↔ l = []
  split; intros; [| by subst].A: Type
l: list A
H: set_eq l []
l = []
  destruct l as [| hd tl]; [done |].A: Type
hd: A
tl: list A
H: set_eq (hd :: tl) []
hd :: tl = []
  destruct H.A: Type
hd: A
tl: list A
H: hd :: tl ⊆ []
H0: [] ⊆ hd :: tl
hd :: tl = []
  specialize (H hd (elem_of_list_here hd tl)).A: Type
hd: A
tl: list A
H: hd ∈ []
H0: [] ⊆ hd :: tl
hd :: tl = []
  by inversion H.
Qed.

Lemma set_eq_cons {A} : forall (a : A) (s1 s2 : set A),
  set_eq s1 s2 ->
  set_eq (a :: s1) (a :: s2).A: Type
∀ (a : A) (s1 s2 : set A),
  set_eq s1 s2 → set_eq (a :: s1) (a :: s2)
Proof.A: Type
∀ (a : A) (s1 s2 : set A),
  set_eq s1 s2 → set_eq (a :: s1) (a :: s2)
  intros a s1 s2 Heq.A: Type
a: A
s1, s2: set A
Heq: set_eq s1 s2
set_eq (a :: s1) (a :: s2)
  rewrite !set_eq_extract_forall in *.A: Type
a: A
s1, s2: set A
Heq: ∀ a : A, a ∈ s1 ↔ a ∈ s2
∀ a0 : A, a0 ∈ a :: s1 ↔ a0 ∈ a :: s2
  setoid_rewrite elem_of_cons.A: Type
a: A
s1, s2: set A
Heq: ∀ a : A, a ∈ s1 ↔ a ∈ s2
∀ a0 : A, a0 = a ∨ a0 ∈ s1 ↔ a0 = a ∨ a0 ∈ s2
  by firstorder.
Qed.

Lemma set_eq_Forall
  {A : Type}
  (s1 s2 : set A)
  (H12 : set_eq s1 s2)
  (P : A -> Prop)
  : Forall P s1 <-> Forall P s2.A: Type
s1, s2: set A
H12: set_eq s1 s2
P: A → Prop
Forall P s1 ↔ Forall P s2
Proof.A: Type
s1, s2: set A
H12: set_eq s1 s2
P: A → Prop
Forall P s1 ↔ Forall P s2
  by rewrite !Forall_forall; firstorder.
Qed.

Lemma set_union_comm `{EqDecision A}  : forall (s1 s2 : list A),
  set_eq (set_union s1 s2) (set_union s2 s1).A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A,
  set_eq (set_union s1 s2) (set_union s2 s1)
Proof.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A,
  set_eq (set_union s1 s2) (set_union s2 s1)
  by intros s1 s2; split; intro x; rewrite !set_union_iff; itauto.
Qed.

Lemma set_union_empty `{EqDecision A}  : forall (s1 s2 : list A),
  set_union s1 s2 = [] ->
  s1 = [] /\ s2 = [].A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A,
  set_union s1 s2 = [] → s1 = [] ∧ s2 = []
Proof.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A,
  set_union s1 s2 = [] → s1 = [] ∧ s2 = []
  intros.A: Type
EqDecision0: EqDecision A
s1, s2: list A
H: set_union s1 s2 = []
s1 = [] ∧ s2 = []
  destruct s2; [done |].A: Type
EqDecision0: EqDecision A
s1: list A
a: A
s2: list A
H: set_union s1 (a :: s2) = []
s1 = [] ∧ a :: s2 = []
  by cbn in H; apply set_add_not_empty in H.
Qed.

Lemma set_union_nodup_left `{EqDecision A} (l l' : set A)
  : NoDup l -> NoDup (set_union l l').A: Type
EqDecision0: EqDecision A
l, l': set A
NoDup l → NoDup (set_union l l')
Proof.A: Type
EqDecision0: EqDecision A
l, l': set A
NoDup l → NoDup (set_union l l')
  intro Hl.A: Type
EqDecision0: EqDecision A
l, l': set A
Hl: NoDup l
NoDup (set_union l l')
  induction l' as [| x' l' IH]; [done |].A: Type
EqDecision0: EqDecision A
l: set A
x': A
l': list A
Hl: NoDup l
IH: NoDup (set_union l l')
NoDup (set_union l (x' :: l'))
  by apply set_add_nodup.
Qed.

Lemma set_union_subseteq_left `{EqDecision A}  : forall (s1 s2 : list A),
  s1 ⊆ set_union s1 s2.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A, s1 ⊆ set_union s1 s2
Proof.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A, s1 ⊆ set_union s1 s2
  by intros; intros x H; apply set_union_intro; left.
Qed.

Lemma set_union_subseteq_right `{EqDecision A}  : forall (s1 s2 : list A),
  s2 ⊆ set_union s1 s2.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A, s2 ⊆ set_union s1 s2
Proof.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A, s2 ⊆ set_union s1 s2
  by intros; intros x H; apply set_union_intro; right.
Qed.

Lemma set_union_subseteq_iff `{EqDecision A}  : forall (s1 s2 s : list A),
  set_union s1 s2 ⊆ s <-> s1 ⊆ s /\ s2 ⊆ s.A: Type
EqDecision0: EqDecision A
∀ s1 s2 s : list A,
  set_union s1 s2 ⊆ s ↔ s1 ⊆ s ∧ s2 ⊆ s
Proof.A: Type
EqDecision0: EqDecision A
∀ s1 s2 s : list A,
  set_union s1 s2 ⊆ s ↔ s1 ⊆ s ∧ s2 ⊆ s
  intros.A: Type
EqDecision0: EqDecision A
s1, s2, s: list A
set_union s1 s2 ⊆ s ↔ s1 ⊆ s ∧ s2 ⊆ s
  unfold subseteq, list_subseteq.A: Type
EqDecision0: EqDecision A
s1, s2, s: list A
(∀ x : A, x ∈ set_union s1 s2 → x ∈ s)
↔ (∀ x : A, x ∈ s1 → x ∈ s)
  ∧ (∀ x : A, x ∈ s2 → x ∈ s)
  setoid_rewrite set_union_iff.A: Type
EqDecision0: EqDecision A
s1, s2, s: list A
(∀ x : A, x ∈ s1 ∨ x ∈ s2 → x ∈ s)
↔ (∀ x : A, x ∈ s1 → x ∈ s)
  ∧ (∀ x : A, x ∈ s2 → x ∈ s)
  by firstorder.
Qed.

Lemma set_union_iterated_nodup `{EqDecision A}
  (ss : list (list A))
  (H : forall s, s ∈ ss -> NoDup s) :
  NoDup (fold_right set_union [] ss).A: Type
EqDecision0: EqDecision A
ss: list (list A)
H: ∀ s : list A, s ∈ ss → NoDup s
NoDup (foldr set_union [] ss)
Proof.A: Type
EqDecision0: EqDecision A
ss: list (list A)
H: ∀ s : list A, s ∈ ss → NoDup s
NoDup (foldr set_union [] ss)
  induction ss; cbn.A: Type
EqDecision0: EqDecision A
H: ∀ s : list A, s ∈ [] → NoDup s
NoDup []
A: Type
EqDecision0: EqDecision A
a: list A
ss: list (list A)
H: ∀ s : list A, s ∈ a :: ss → NoDup s
IHss: (∀ s : list A, s ∈ ss → NoDup s)
→ NoDup (foldr set_union [] ss)
NoDup (set_union a (foldr set_union [] ss))
  -A: Type
EqDecision0: EqDecision A
H: ∀ s : list A, s ∈ [] → NoDup s
NoDup [] by apply NoDup_nil.
  -A: Type
EqDecision0: EqDecision A
a: list A
ss: list (list A)
H: ∀ s : list A, s ∈ a :: ss → NoDup s
IHss: (∀ s : list A, s ∈ ss → NoDup s)
→ NoDup (foldr set_union [] ss)
NoDup (set_union a (foldr set_union [] ss)) apply set_union_nodup.A: Type
EqDecision0: EqDecision A
a: list A
ss: list (list A)
H: ∀ s : list A, s ∈ a :: ss → NoDup s
IHss: (∀ s : list A, s ∈ ss → NoDup s)
→ NoDup (foldr set_union [] ss)
NoDup a
A: Type
EqDecision0: EqDecision A
a: list A
ss: list (list A)
H: ∀ s : list A, s ∈ a :: ss → NoDup s
IHss: (∀ s : list A, s ∈ ss → NoDup s)
→ NoDup (foldr set_union [] ss)
NoDup (foldr set_union [] ss)
    +A: Type
EqDecision0: EqDecision A
a: list A
ss: list (list A)
H: ∀ s : list A, s ∈ a :: ss → NoDup s
IHss: (∀ s : list A, s ∈ ss → NoDup s)
→ NoDup (foldr set_union [] ss)
NoDup a by apply H; left.
    +A: Type
EqDecision0: EqDecision A
a: list A
ss: list (list A)
H: ∀ s : list A, s ∈ a :: ss → NoDup s
IHss: (∀ s : list A, s ∈ ss → NoDup s)
→ NoDup (foldr set_union [] ss)
NoDup (foldr set_union [] ss) by apply IHss; intros; apply H; right.
Qed.

Lemma set_union_in_iterated
  `{EqDecision A}
  (ss : list (set A))
  (a : A)
  : a ∈ fold_right set_union [] ss <-> Exists (fun s => a ∈ s) ss.A: Type
EqDecision0: EqDecision A
ss: list (set A)
a: A
a ∈ foldr set_union [] ss
↔ Exists (λ s : set A, a ∈ s) ss
Proof.A: Type
EqDecision0: EqDecision A
ss: list (set A)
a: A
a ∈ foldr set_union [] ss
↔ Exists (λ s : set A, a ∈ s) ss
  rewrite Exists_exists.A: Type
EqDecision0: EqDecision A
ss: list (set A)
a: A
a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
  induction ss; split; simpl.A: Type
EqDecision0: EqDecision A
a: A
a ∈ [] → ∃ x : set A, x ∈ [] ∧ a ∈ x
A: Type
EqDecision0: EqDecision A
a: A
(∃ x : set A, x ∈ [] ∧ a ∈ x) → a ∈ []
A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
a ∈ set_union a0 (foldr set_union [] ss)
→ ∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x
A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
(∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x)
→ a ∈ set_union a0 (foldr set_union [] ss)
  -A: Type
EqDecision0: EqDecision A
a: A
a ∈ [] → ∃ x : set A, x ∈ [] ∧ a ∈ x by intro H; inversion H.
  -A: Type
EqDecision0: EqDecision A
a: A
(∃ x : set A, x ∈ [] ∧ a ∈ x) → a ∈ [] by intros (x & Hin & _); inversion Hin.
  -A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
a ∈ set_union a0 (foldr set_union [] ss)
→ ∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x intro Hin; apply set_union_iff in Hin as [Hina0 | Hinss].A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
Hina0: a ∈ a0
∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x
A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
Hinss: a ∈ foldr set_union [] ss
∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x
    +A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
Hina0: a ∈ a0
∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x by exists a0; rewrite elem_of_cons; split; [left |].
    +A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
Hinss: a ∈ foldr set_union [] ss
∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x apply IHss in Hinss as (x & Hinss & Hinx).A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
x: set A
Hinss: x ∈ ss
Hinx: a ∈ x
∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x
      by setoid_rewrite elem_of_cons; eauto.
  -A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
(∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x)
→ a ∈ set_union a0 (foldr set_union [] ss) rewrite set_union_iff.A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
(∃ x : set A, x ∈ a0 :: ss ∧ a ∈ x)
→ a ∈ a0 ∨ a ∈ foldr set_union [] ss
    intros (x & Hx & Ha).A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
x: set A
Hx: x ∈ a0 :: ss
Ha: a ∈ x
a ∈ a0 ∨ a ∈ foldr set_union [] ss
    apply elem_of_cons in Hx as [-> |].A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
Ha: a ∈ a0
a ∈ a0 ∨ a ∈ foldr set_union [] ss
A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
x: set A
H: x ∈ ss
Ha: a ∈ x
a ∈ a0 ∨ a ∈ foldr set_union [] ss
    +A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
Ha: a ∈ a0
a ∈ a0 ∨ a ∈ foldr set_union [] ss by left.
    +A: Type
EqDecision0: EqDecision A
a0: set A
ss: list (set A)
a: A
IHss: a ∈ foldr set_union [] ss
↔ (∃ x : set A, x ∈ ss ∧ a ∈ x)
x: set A
H: x ∈ ss
Ha: a ∈ x
a ∈ a0 ∨ a ∈ foldr set_union [] ss by right; apply IHss; exists x.
Qed.

Lemma set_union_iterated_subseteq
  `{EqDecision A}
  (ss ss' : list (set A))
  (Hincl : ss ⊆ ss') :
  fold_right set_union [] ss ⊆
  fold_right set_union [] ss'.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
foldr set_union [] ss ⊆ foldr set_union [] ss'
Proof.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
foldr set_union [] ss ⊆ foldr set_union [] ss'
  intros a H.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
a: A
H: a ∈ foldr set_union [] ss
a ∈ foldr set_union [] ss'
  apply set_union_in_iterated in H.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
a: A
H: Exists (λ s : set A, a ∈ s) ss
a ∈ foldr set_union [] ss'
  apply set_union_in_iterated.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
a: A
H: Exists (λ s : set A, a ∈ s) ss
Exists (λ s : set A, a ∈ s) ss'
  rewrite Exists_exists in *.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
a: A
H: ∃ x : set A, x ∈ ss ∧ a ∈ x
∃ x : set A, x ∈ ss' ∧ a ∈ x
  destruct H as [x [Hx Ha]].A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
a: A
x: set A
Hx: x ∈ ss
Ha: a ∈ x
∃ x : set A, x ∈ ss' ∧ a ∈ x
  exists x.A: Type
EqDecision0: EqDecision A
ss, ss': list (set A)
Hincl: ss ⊆ ss'
a: A
x: set A
Hx: x ∈ ss
Ha: a ∈ x
x ∈ ss' ∧ a ∈ x
  by split; [apply Hincl |].
Qed.

Lemma set_union_empty_left `{EqDecision A}  : forall (s : list A),
  NoDup s -> set_eq (set_union [] s) s.A: Type
EqDecision0: EqDecision A
∀ s : list A, NoDup s → set_eq (set_union [] s) s
Proof.A: Type
EqDecision0: EqDecision A
∀ s : list A, NoDup s → set_eq (set_union [] s) s
  intros.A: Type
EqDecision0: EqDecision A
s: list A
H: NoDup s
set_eq (set_union [] s) s split; intros x Hin.A: Type
EqDecision0: EqDecision A
s: list A
H: NoDup s
x: A
Hin: x ∈ set_union [] s
x ∈ s
A: Type
EqDecision0: EqDecision A
s: list A
H: NoDup s
x: A
Hin: x ∈ s
x ∈ set_union [] s
  -A: Type
EqDecision0: EqDecision A
s: list A
H: NoDup s
x: A
Hin: x ∈ set_union [] s
x ∈ s by apply set_union_elim in Hin as []; [inversion H0 |].
  -A: Type
EqDecision0: EqDecision A
s: list A
H: NoDup s
x: A
Hin: x ∈ s
x ∈ set_union [] s by apply set_union_intro; right.
Qed.

Lemma map_list_subseteq {A B} : forall (f : B -> A) (s s' : list B),
  s ⊆ s' -> map f s ⊆ map f s'.A, B: Type
∀ (f : B → A) (s s' : list B),
  s ⊆ s' → map f s ⊆ map f s'
Proof.A, B: Type
∀ (f : B → A) (s s' : list B),
  s ⊆ s' → map f s ⊆ map f s'
  intro f; induction s; intros; simpl.A, B: Type
f: B → A
s': list B
H: [] ⊆ s'
[] ⊆ map f s'
A, B: Type
f: B → A
a: B
s: list B
IHs: ∀ s' : list B, s ⊆ s' → map f s ⊆ map f s'
s': list B
H: a :: s ⊆ s'
f a :: map f s ⊆ map f s'
  -A, B: Type
f: B → A
s': list B
H: [] ⊆ s'
[] ⊆ map f s' by apply list_subseteq_nil.
  -A, B: Type
f: B → A
a: B
s: list B
IHs: ∀ s' : list B, s ⊆ s' → map f s ⊆ map f s'
s': list B
H: a :: s ⊆ s'
f a :: map f s ⊆ map f s' assert (Hs : s ⊆ s') by (intros b Hs; apply H; right; done).A, B: Type
f: B → A
a: B
s: list B
IHs: ∀ s' : list B, s ⊆ s' → map f s ⊆ map f s'
s': list B
H: a :: s ⊆ s'
Hs: s ⊆ s'
f a :: map f s ⊆ map f s'
    specialize (IHs s' Hs).A, B: Type
f: B → A
a: B
s, s': list B
IHs: map f s ⊆ map f s'
H: a :: s ⊆ s'
Hs: s ⊆ s'
f a :: map f s ⊆ map f s'
    intros b Hs'.A, B: Type
f: B → A
a: B
s, s': list B
IHs: map f s ⊆ map f s'
H: a :: s ⊆ s'
Hs: s ⊆ s'
b: A
Hs': b ∈ f a :: map f s
b ∈ map f s'
    apply elem_of_cons in Hs' as [-> |]; [| by apply IHs].A, B: Type
f: B → A
a: B
s, s': list B
IHs: map f s ⊆ map f s'
H: a :: s ⊆ s'
Hs: s ⊆ s'
f a ∈ map f s'
    by apply elem_of_list_fmap_1, H; left.
Qed.

Lemma map_set_eq {A B} (f : B -> A) : forall s s',
  set_eq s s' ->
  set_eq (map f s) (map f s').A, B: Type
f: B → A
∀ s s' : set B,
  set_eq s s' → set_eq (map f s) (map f s')
Proof.A, B: Type
f: B → A
∀ s s' : set B,
  set_eq s s' → set_eq (map f s) (map f s')
  by split; apply map_list_subseteq; apply H.
Qed.

Lemma set_map_nodup {A B} `{EqDecision A} (f : B -> A) : forall (s : set B),
  NoDup (set_map f s).A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ s : set B, NoDup (set_map f s)
Proof.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ s : set B, NoDup (set_map f s)
  induction s; simpl; try constructor.A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: NoDup (set_map f s)
NoDup (set_add (f a) (set_map f s))
  by apply set_add_nodup.
Qed.

Lemma set_map_elem_of {A B} `{EqDecision A} (f : B -> A) : forall x s,
  x ∈ s ->
  f x ∈ set_map f s.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ (x : B) (s : set B), x ∈ s → f x ∈ set_map f s
Proof.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ (x : B) (s : set B), x ∈ s → f x ∈ set_map f s
  induction s; intros; inversion H; subst; clear H; simpl.A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: a ∈ s → f a ∈ set_map f s
f a ∈ set_add (f a) (set_map f s)
A, B: Type
EqDecision0: EqDecision A
f: B → A
x, a: B
s: list B
IHs: x ∈ s → f x ∈ set_map f s
H2: x ∈ s
f x ∈ set_add (f a) (set_map f s)
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: a ∈ s → f a ∈ set_map f s
f a ∈ set_add (f a) (set_map f s) by apply set_add_intro2.
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
x, a: B
s: list B
IHs: x ∈ s → f x ∈ set_map f s
H2: x ∈ s
f x ∈ set_add (f a) (set_map f s) by apply set_add_intro1, IHs.
Qed.

Lemma set_map_exists {A B} `{EqDecision A} (f : B -> A) : forall y s,
  y ∈ set_map f s <->
  exists x, x ∈ s /\ f x = y.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ (y : A) (s : set B),
  y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
Proof.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ (y : A) (s : set B),
  y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
  induction s; split; intros; cbn in *.A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
H: y ∈ empty_set
∃ x : B, x ∈ [] ∧ f x = y
A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
H: ∃ x : B, x ∈ [] ∧ f x = y
y ∈ empty_set
A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
a: B
s: list B
IHs: y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
H: y
∈ set_add (f a)
    (foldr (λ a : B, set_add (f a)) empty_set s)
∃ x : B, x ∈ a :: s ∧ f x = y
A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
a: B
s: list B
IHs: y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
H: ∃ x : B, x ∈ a :: s ∧ f x = y
y
∈ set_add (f a)
    (foldr (λ a : B, set_add (f a)) empty_set s)
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
H: y ∈ empty_set
∃ x : B, x ∈ [] ∧ f x = y by inversion H.
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
H: ∃ x : B, x ∈ [] ∧ f x = y
y ∈ empty_set by destruct H as (x & Hx & Hf); inversion Hx.
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
a: B
s: list B
IHs: y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
H: y
∈ set_add (f a)
    (foldr (λ a : B, set_add (f a)) empty_set s)
∃ x : B, x ∈ a :: s ∧ f x = y apply set_add_iff in H as [Heq | Hin]; subst.A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: f a ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = f a)
∃ x : B, x ∈ a :: s ∧ f x = f a
A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
a: B
s: list B
IHs: y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
Hin: y ∈ foldr (λ a : B, set_add (f a)) empty_set s
∃ x : B, x ∈ a :: s ∧ f x = y
    +A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: f a ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = f a)
∃ x : B, x ∈ a :: s ∧ f x = f a by exists a; split; [left |].
    +A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
a: B
s: list B
IHs: y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
Hin: y ∈ foldr (λ a : B, set_add (f a)) empty_set s
∃ x : B, x ∈ a :: s ∧ f x = y apply IHs in Hin as (x & Hin & Heq); subst.A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
x: B
IHs: f x ∈ set_map f s
↔ (∃ x0 : B, x0 ∈ s ∧ f x0 = f x)
Hin: x ∈ s
∃ x0 : B, x0 ∈ a :: s ∧ f x0 = f x
      by exists x; split; [right |].
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
y: A
a: B
s: list B
IHs: y ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = y)
H: ∃ x : B, x ∈ a :: s ∧ f x = y
y
∈ set_add (f a)
    (foldr (λ a : B, set_add (f a)) empty_set s) destruct H as [x [Hx Hf]]; subst; simpl; apply set_add_iff.A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
x: B
IHs: f x ∈ set_map f s
↔ (∃ x0 : B, x0 ∈ s ∧ f x0 = f x)
Hx: x ∈ a :: s
f x = f a
∨ f x ∈ foldr (λ a : B, set_add (f a)) empty_set s
    apply elem_of_cons in Hx as [-> |].A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: f a ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = f a)
f a = f a
∨ f a ∈ foldr (λ a : B, set_add (f a)) empty_set s
A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
x: B
IHs: f x ∈ set_map f s
↔ (∃ x0 : B, x0 ∈ s ∧ f x0 = f x)
H: x ∈ s
f x = f a
∨ f x ∈ foldr (λ a : B, set_add (f a)) empty_set s
    +A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: f a ∈ set_map f s ↔ (∃ x : B, x ∈ s ∧ f x = f a)
f a = f a
∨ f a ∈ foldr (λ a : B, set_add (f a)) empty_set s by left.
    +A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
x: B
IHs: f x ∈ set_map f s
↔ (∃ x0 : B, x0 ∈ s ∧ f x0 = f x)
H: x ∈ s
f x = f a
∨ f x ∈ foldr (λ a : B, set_add (f a)) empty_set s by right; apply IHs; exists x.
Qed.

Lemma set_map_subseteq {A B} `{EqDecision A} (f : B -> A) : forall s s',
  s ⊆ s' ->
  set_map f s ⊆ set_map f s'.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ s s' : set B, s ⊆ s' → set_map f s ⊆ set_map f s'
Proof.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ s s' : set B, s ⊆ s' → set_map f s ⊆ set_map f s'
  induction s; cbn; intros s' Hsub msg Hin; [by inversion Hin |].A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: ∀ s' : set B,
  s ⊆ s' → set_map f s ⊆ set_map f s'
s': set B
Hsub: a :: s ⊆ s'
msg: A
Hin: msg
∈ set_add (f a)
    (foldr (λ a : B, set_add (f a)) empty_set s)
msg ∈ set_map f s'
  apply set_add_elim in Hin as [-> |].A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: ∀ s' : set B,
  s ⊆ s' → set_map f s ⊆ set_map f s'
s': set B
Hsub: a :: s ⊆ s'
f a ∈ set_map f s'
A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: ∀ s' : set B,
  s ⊆ s' → set_map f s ⊆ set_map f s'
s': set B
Hsub: a :: s ⊆ s'
msg: A
H: msg ∈ foldr (λ a : B, set_add (f a)) empty_set s
msg ∈ set_map f s'
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: ∀ s' : set B,
  s ⊆ s' → set_map f s ⊆ set_map f s'
s': set B
Hsub: a :: s ⊆ s'
f a ∈ set_map f s' by apply set_map_elem_of, Hsub; left.
  -A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: ∀ s' : set B,
  s ⊆ s' → set_map f s ⊆ set_map f s'
s': set B
Hsub: a :: s ⊆ s'
msg: A
H: msg ∈ foldr (λ a : B, set_add (f a)) empty_set s
msg ∈ set_map f s' apply IHs; [| done].A, B: Type
EqDecision0: EqDecision A
f: B → A
a: B
s: list B
IHs: ∀ s' : set B,
  s ⊆ s' → set_map f s ⊆ set_map f s'
s': set B
Hsub: a :: s ⊆ s'
msg: A
H: msg ∈ foldr (λ a : B, set_add (f a)) empty_set s
s ⊆ s'
    by intros x Hin'; apply Hsub; right.
Qed.

Lemma set_map_eq {A B} `{EqDecision A} (f : B -> A) : forall s s',
  set_eq s s' ->
  set_eq (set_map f s) (set_map f s').A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ s s' : set B,
  set_eq s s' → set_eq (set_map f s) (set_map f s')
Proof.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ s s' : set B,
  set_eq s s' → set_eq (set_map f s) (set_map f s')
  by split; destruct H; apply set_map_subseteq.
Qed.

Lemma set_map_singleton {A B} `{EqDecision A} (f : B -> A) : forall s a,
  set_map f s = [a] ->
  forall b, b ∈ s -> f b = a.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ (s : set B) (a : A),
  set_map f s = [a] → ∀ b : B, b ∈ s → f b = a
Proof.A, B: Type
EqDecision0: EqDecision A
f: B → A
∀ (s : set B) (a : A),
  set_map f s = [a] → ∀ b : B, b ∈ s → f b = a
  intros s a H b H0.A, B: Type
EqDecision0: EqDecision A
f: B → A
s: set B
a: A
H: set_map f s = [a]
b: B
H0: b ∈ s
f b = a
  apply (set_map_elem_of f) in H0.A, B: Type
EqDecision0: EqDecision A
f: B → A
s: set B
a: A
H: set_map f s = [a]
b: B
H0: f b ∈ set_map f s
f b = a
  rewrite H in H0.A, B: Type
EqDecision0: EqDecision A
f: B → A
s: set B
a: A
H: set_map f s = [a]
b: B
H0: f b ∈ [a]
f b = a
  by apply elem_of_cons in H0 as []; [| inversion H0].
Qed.

Lemma filter_set_add `{EqDecision X} P
  `{forall (x : X), Decision (P x)} :
  forall (l : list X) x, ~ P x ->
  filter P l = filter P (set_add x l).X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
∀ (l : list X) (x : X),
  ¬ P x → filter P l = filter P (set_add x l)
Proof.X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
∀ (l : list X) (x : X),
  ¬ P x → filter P l = filter P (set_add x l)
  induction l as [| hd tl IHl]; intros x H_false; cbn.X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
x: X
H_false: ¬ P x
[] = (if decide (P x) then [x] else [])
X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
hd: X
tl: list X
IHl: ∀ x : X,
  ¬ P x → filter P tl = filter P (set_add x tl)
x: X
H_false: ¬ P x
(if decide (P hd)
 then hd :: filter P tl
 else filter P tl) =
filter P
  (if decide (x = hd)
   then hd :: tl
   else hd :: set_add x tl)
  -X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
x: X
H_false: ¬ P x
[] = (if decide (P x) then [x] else []) by rewrite decide_False.
  -X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
hd: X
tl: list X
IHl: ∀ x : X,
  ¬ P x → filter P tl = filter P (set_add x tl)
x: X
H_false: ¬ P x
(if decide (P hd)
 then hd :: filter P tl
 else filter P tl) =
filter P
  (if decide (x = hd)
   then hd :: tl
   else hd :: set_add x tl) destruct (decide (x = hd)); cbn; [done |].X: Type
EqDecision0: EqDecision X
P: X → Prop
H: ∀ x : X, Decision (P x)
hd: X
tl: list X
IHl: ∀ x : X,
  ¬ P x → filter P tl = filter P (set_add x tl)
x: X
H_false: ¬ P x
n: x ≠ hd
(if decide (P hd)
 then hd :: filter P tl
 else filter P tl) =
(if decide (P hd)
 then hd :: filter P (set_add x tl)
 else filter P (set_add x tl))
    by destruct (decide (P hd)); rewrite <- IHl.
Qed.

Lemma set_add_ignore `{EqDecision X} :
  forall (l : list X) (x : X),
    x ∈ l ->
    set_add x l = l.X: Type
EqDecision0: EqDecision X
∀ (l : list X) (x : X), x ∈ l → set_add x l = l
Proof.X: Type
EqDecision0: EqDecision X
∀ (l : list X) (x : X), x ∈ l → set_add x l = l
  induction l as [| hd tl IHl]; inversion 1; subst; cbn.X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHl: ∀ x : X, x ∈ tl → set_add x tl = tl
H: hd ∈ hd :: tl
(if decide (hd = hd)
 then hd :: tl
 else hd :: set_add hd tl) = 
hd :: tl
X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHl: ∀ x : X, x ∈ tl → set_add x tl = tl
x: X
H: x ∈ hd :: tl
H2: x ∈ tl
(if decide (x = hd)
 then hd :: tl
 else hd :: set_add x tl) = 
hd :: tl
  -X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHl: ∀ x : X, x ∈ tl → set_add x tl = tl
H: hd ∈ hd :: tl
(if decide (hd = hd)
 then hd :: tl
 else hd :: set_add hd tl) = 
hd :: tl by rewrite decide_True.
  -X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHl: ∀ x : X, x ∈ tl → set_add x tl = tl
x: X
H: x ∈ hd :: tl
H2: x ∈ tl
(if decide (x = hd)
 then hd :: tl
 else hd :: set_add x tl) = 
hd :: tl by case_decide; [| rewrite IHl].
Qed.

Lemma set_add_new `{EqDecision A} :
  forall (x : A) l, x ∉ l -> set_add x l = l++[x].A: Type
EqDecision0: EqDecision A
∀ (x : A) (l : set A), x ∉ l → set_add x l = l ++ [x]
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (l : set A), x ∉ l → set_add x l = l ++ [x]
  induction l; cbn; [done |]; intros H_not_in.A: Type
EqDecision0: EqDecision A
x, a: A
l: list A
IHl: x ∉ l → set_add x l = l ++ [x]
H_not_in: x ∉ a :: l
(if decide (x = a) then a :: l else a :: set_add x l) =
a :: l ++ [x]
  rewrite decide_False; cycle 1.A: Type
EqDecision0: EqDecision A
x, a: A
l: list A
IHl: x ∉ l → set_add x l = l ++ [x]
H_not_in: x ∉ a :: l
x ≠ a
A: Type
EqDecision0: EqDecision A
x, a: A
l: list A
IHl: x ∉ l → set_add x l = l ++ [x]
H_not_in: x ∉ a :: l
a :: set_add x l = a :: l ++ [x]
  -A: Type
EqDecision0: EqDecision A
x, a: A
l: list A
IHl: x ∉ l → set_add x l = l ++ [x]
H_not_in: x ∉ a :: l
x ≠ a by intros ->; apply H_not_in; left.
  -A: Type
EqDecision0: EqDecision A
x, a: A
l: list A
IHl: x ∉ l → set_add x l = l ++ [x]
H_not_in: x ∉ a :: l
a :: set_add x l = a :: l ++ [x] by rewrite elem_of_cons in H_not_in; rewrite IHl; itauto.
Qed.

Lemma set_remove_not_elem_of `{EqDecision A} : forall x (s : list A),
  x ∉ s ->
  set_remove x s = s.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s : list A), x ∉ s → set_remove x s = s
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s : list A), x ∉ s → set_remove x s = s
  induction s; cbn; intros; [done |].A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: x ∉ s → set_remove x s = s
H: x ∉ a :: s
(if decide (x = a) then s else a :: set_remove x s) =
a :: s
  rewrite decide_False; cycle 1.A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: x ∉ s → set_remove x s = s
H: x ∉ a :: s
x ≠ a
A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: x ∉ s → set_remove x s = s
H: x ∉ a :: s
a :: set_remove x s = a :: s
  -A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: x ∉ s → set_remove x s = s
H: x ∉ a :: s
x ≠ a by intros ->; contradict H; left.
  -A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: x ∉ s → set_remove x s = s
H: x ∉ a :: s
a :: set_remove x s = a :: s rewrite IHs; [done |].A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: x ∉ s → set_remove x s = s
H: x ∉ a :: s
x ∉ s
    by rewrite elem_of_cons in H; itauto.
Qed.

Lemma set_remove_elim `{EqDecision A} : forall x (s : list A),
  NoDup s -> x ∉ set_remove x s.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s : list A), NoDup s → x ∉ set_remove x s
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s : list A), NoDup s → x ∉ set_remove x s
  by intros x s HND Hnelem; apply set_remove_iff in Hnelem; itauto.
Qed.

Lemma set_remove_first `{EqDecision A} : forall x y (s : list A),
  x = y -> set_remove x (y :: s) = s.A: Type
EqDecision0: EqDecision A
∀ (x y : A) (s : list A),
  x = y → set_remove x (y :: s) = s
Proof.A: Type
EqDecision0: EqDecision A
∀ (x y : A) (s : list A),
  x = y → set_remove x (y :: s) = s
  by intros x y s ->; cbn; rewrite decide_True.
Qed.

Lemma set_remove_nodup_1 `{EqDecision A} : forall x (s : list A),
  NoDup (set_remove x s) ->
  x ∉ set_remove x s ->
  NoDup s.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s : list A),
  NoDup (set_remove x s)
  → x ∉ set_remove x s → NoDup s
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s : list A),
  NoDup (set_remove x s)
  → x ∉ set_remove x s → NoDup s
  induction s; intros; [by constructor |].A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: NoDup (set_remove x s)
→ x ∉ set_remove x s → NoDup s
H: NoDup (set_remove x (a :: s))
H0: x ∉ set_remove x (a :: s)
NoDup (a :: s)
  simpl in H0; destruct (decide (x = a)); subst.A: Type
EqDecision0: EqDecision A
a: A
s: list A
H: NoDup (set_remove a (a :: s))
IHs: NoDup (set_remove a s)
→ a ∉ set_remove a s → NoDup s
H0: a ∉ s
NoDup (a :: s)
A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: NoDup (set_remove x s)
→ x ∉ set_remove x s → NoDup s
H: NoDup (set_remove x (a :: s))
n: x ≠ a
H0: x ∉ a :: set_remove x s
NoDup (a :: s)
  -A: Type
EqDecision0: EqDecision A
a: A
s: list A
H: NoDup (set_remove a (a :: s))
IHs: NoDup (set_remove a s)
→ a ∉ set_remove a s → NoDup s
H0: a ∉ s
NoDup (a :: s) by cbn in H; rewrite decide_True in H; constructor.
  -A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: NoDup (set_remove x s)
→ x ∉ set_remove x s → NoDup s
H: NoDup (set_remove x (a :: s))
n: x ≠ a
H0: x ∉ a :: set_remove x s
NoDup (a :: s) rewrite elem_of_cons in H0.A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: NoDup (set_remove x s)
→ x ∉ set_remove x s → NoDup s
H: NoDup (set_remove x (a :: s))
n: x ≠ a
H0: ¬ (x = a ∨ x ∈ set_remove x s)
NoDup (a :: s)
    simpl in H; rewrite decide_False in H by done; inversion H; subst; clear H.A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: NoDup (set_remove x s)
→ x ∉ set_remove x s → NoDup s
n: x ≠ a
H0: ¬ (x = a ∨ x ∈ set_remove x s)
H3: a ∉ set_remove x s
H4: NoDup (set_remove x s)
NoDup (a :: s)
    constructor; [| by firstorder].A: Type
EqDecision0: EqDecision A
x, a: A
s: list A
IHs: NoDup (set_remove x s)
→ x ∉ set_remove x s → NoDup s
n: x ≠ a
H0: ¬ (x = a ∨ x ∈ set_remove x s)
H3: a ∉ set_remove x s
H4: NoDup (set_remove x s)
a ∉ s
    by intro Ha; apply (set_remove_3 _ x) in Ha; auto.
Qed.

Lemma set_remove_elem_of_iff `{EqDecision A} :  forall x y (s : list A),
  NoDup s ->
  y ∈ s ->
  x ∈ s <-> x = y \/ x ∈ set_remove y s.A: Type
EqDecision0: EqDecision A
∀ (x y : A) (s : list A),
  NoDup s → y ∈ s → x ∈ s ↔ x = y ∨ x ∈ set_remove y s
Proof.A: Type
EqDecision0: EqDecision A
∀ (x y : A) (s : list A),
  NoDup s → y ∈ s → x ∈ s ↔ x = y ∨ x ∈ set_remove y s
  intros.A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
x ∈ s ↔ x = y ∨ x ∈ set_remove y s split; intros.A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x ∈ s
x = y ∨ x ∈ set_remove y s
A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x = y ∨ x ∈ set_remove y s
x ∈ s
  -A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x ∈ s
x = y ∨ x ∈ set_remove y s destruct (decide (x = y)).A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x ∈ s
e: x = y
x = y ∨ x ∈ set_remove y s
A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x ∈ s
n: x ≠ y
x = y ∨ x ∈ set_remove y s
    +A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x ∈ s
e: x = y
x = y ∨ x ∈ set_remove y s by left.
    +A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x ∈ s
n: x ≠ y
x = y ∨ x ∈ set_remove y s by right; apply set_remove_3.
  -A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
H1: x = y ∨ x ∈ set_remove y s
x ∈ s destruct H1 as [Heq | Hin].A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
Heq: x = y
x ∈ s
A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
Hin: x ∈ set_remove y s
x ∈ s
    +A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
Heq: x = y
x ∈ s by subst.
    +A: Type
EqDecision0: EqDecision A
x, y: A
s: list A
H: NoDup s
H0: y ∈ s
Hin: x ∈ set_remove y s
x ∈ s by apply set_remove_1 in Hin.
Qed.

Lemma set_add_length
  `{EqDecision A}
  (x : A)
  (s : set A)
  (Hx : x ∉ s)
  : S (length s) = length (set_add x s).A: Type
EqDecision0: EqDecision A
x: A
s: set A
Hx: x ∉ s
S (length s) = length (set_add x s)
Proof.A: Type
EqDecision0: EqDecision A
x: A
s: set A
Hx: x ∉ s
S (length s) = length (set_add x s)
  revert x Hx.A: Type
EqDecision0: EqDecision A
s: set A
∀ x : A, x ∉ s → S (length s) = length (set_add x s)
  induction s; cbn; intros; [done |].A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∉ s → S (length s) = length (set_add x s)
x: A
Hx: x ∉ a :: s
S (S (length s)) =
length
  (if decide (x = a) then a :: s else a :: set_add x s)
  destruct (decide (x = a)); [by subst; elim Hx; left |].A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∉ s → S (length s) = length (set_add x s)
x: A
Hx: x ∉ a :: s
n: x ≠ a
S (S (length s)) = length (a :: set_add x s)
  cbn; f_equal.A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∉ s → S (length s) = length (set_add x s)
x: A
Hx: x ∉ a :: s
n: x ≠ a
S (length s) = length (set_add x s)
  by apply IHs; intro Hs; apply Hx; right.
Qed.

Lemma set_remove_length
  `{EqDecision A}
  (x : A)
  (s : set A)
  (Hx : x ∈ s)
  : length s = S (length (set_remove x s)).A: Type
EqDecision0: EqDecision A
x: A
s: set A
Hx: x ∈ s
length s = S (length (set_remove x s))
Proof.A: Type
EqDecision0: EqDecision A
x: A
s: set A
Hx: x ∈ s
length s = S (length (set_remove x s))
  generalize dependent x.A: Type
EqDecision0: EqDecision A
s: set A
∀ x : A,
  x ∈ s → length s = S (length (set_remove x s)) induction s; intros; inversion Hx; subst.A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∈ s → length s = S (length (set_remove x s))
Hx: a ∈ a :: s
length (a :: s) = S (length (set_remove a (a :: s)))
A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∈ s → length s = S (length (set_remove x s))
x: A
Hx: x ∈ a :: s
H1: x ∈ s
length (a :: s) = S (length (set_remove x (a :: s)))
  -A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∈ s → length s = S (length (set_remove x s))
Hx: a ∈ a :: s
length (a :: s) = S (length (set_remove a (a :: s))) by rewrite set_remove_first.
  -A: Type
EqDecision0: EqDecision A
a: A
s: list A
IHs: ∀ x : A,
  x ∈ s → length s = S (length (set_remove x s))
x: A
Hx: x ∈ a :: s
H1: x ∈ s
length (a :: s) = S (length (set_remove x (a :: s))) by cbn; destruct (decide (x = a)); [| cbn; rewrite <- IHs].
Qed.

Lemma set_eq_remove `{EqDecision A} : forall x (s1 s2 : list A),
  NoDup s1 ->
  NoDup s2 ->
  set_eq s1 s2 ->
  set_eq (set_remove x s1) (set_remove x s2).A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → set_eq s1 s2
      → set_eq (set_remove x s1) (set_remove x s2)
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → set_eq s1 s2
      → set_eq (set_remove x s1) (set_remove x s2)
  intros x s1 s2 HND1 HND2 [].A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
HND1: NoDup s1
HND2: NoDup s2
H: s1 ⊆ s2
H0: s2 ⊆ s1
set_eq (set_remove x s1) (set_remove x s2)
  by split; intros a Hin; rewrite set_remove_iff in *; itauto.
Qed.

Lemma subseteq_remove_union `{EqDecision A} : forall x (s1 s2 : list A),
  NoDup s1 ->
  NoDup s2 ->
  set_remove x (set_union s1 s2) ⊆
  set_union s1 (set_remove x s2).A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → set_remove x (set_union s1 s2)
      ⊆ set_union s1 (set_remove x s2)
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → set_remove x (set_union s1 s2)
      ⊆ set_union s1 (set_remove x s2)
  intros.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
set_remove x (set_union s1 s2)
⊆ set_union s1 (set_remove x s2) intros y Hin.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
Hin: y ∈ set_remove x (set_union s1 s2)
y ∈ set_union s1 (set_remove x s2) apply set_remove_iff in Hin.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
Hin: y ∈ set_union s1 s2 ∧ y ≠ x
y ∈ set_union s1 (set_remove x s2)
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
Hin: y ∈ set_remove x (set_union s1 s2)
H1: ∀ (a b : A) (l : set A),
  NoDup l → a ∈ set_remove b l → a ∈ l ∧ a ≠ b
NoDup (set_union s1 s2)
  -A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
Hin: y ∈ set_union s1 s2 ∧ y ≠ x
y ∈ set_union s1 (set_remove x s2) apply set_union_intro.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
Hin: y ∈ set_union s1 s2 ∧ y ≠ x
y ∈ s1 ∨ y ∈ set_remove x s2 destruct Hin.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
H1: y ∈ set_union s1 s2
H2: y ≠ x
y ∈ s1 ∨ y ∈ set_remove x s2 apply set_union_elim in H1.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
H1: y ∈ s1 ∨ y ∈ s2
H2: y ≠ x
y ∈ s1 ∨ y ∈ set_remove x s2
    by rewrite set_remove_iff; itauto.
  -A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
y: A
Hin: y ∈ set_remove x (set_union s1 s2)
H1: ∀ (a b : A) (l : set A),
  NoDup l → a ∈ set_remove b l → a ∈ l ∧ a ≠ b
NoDup (set_union s1 s2) by apply set_union_nodup.
Qed.

Lemma set_eq_remove_union_elem_of  `{EqDecision A} : forall x (s1 s2 : list A),
  NoDup s1 ->
  NoDup s2 ->
  x ∈ s1 ->
  set_eq (set_union s1 (set_remove x s2)) (set_union s1 s2).A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → x ∈ s1
      → set_eq (set_union s1 (set_remove x s2))
          (set_union s1 s2)
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → x ∈ s1
      → set_eq (set_union s1 (set_remove x s2))
          (set_union s1 s2)
  split; intros msg Hin; apply set_union_iff; apply set_union_iff in Hin
  ; destruct Hin; try by left.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
msg: A
H2: msg ∈ set_remove x s2
msg ∈ s1 ∨ msg ∈ s2
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
msg: A
H2: msg ∈ s2
msg ∈ s1 ∨ msg ∈ set_remove x s2
  -A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
msg: A
H2: msg ∈ set_remove x s2
msg ∈ s1 ∨ msg ∈ s2 by apply set_remove_iff in H2; itauto.
  -A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
msg: A
H2: msg ∈ s2
msg ∈ s1 ∨ msg ∈ set_remove x s2 destruct (decide (msg = x)); subst.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
H2: x ∈ s2
x ∈ s1 ∨ x ∈ set_remove x s2
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
msg: A
H2: msg ∈ s2
n: msg ≠ x
msg ∈ s1 ∨ msg ∈ set_remove x s2
    +A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
H2: x ∈ s2
x ∈ s1 ∨ x ∈ set_remove x s2 by left.
    +A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∈ s1
msg: A
H2: msg ∈ s2
n: msg ≠ x
msg ∈ s1 ∨ msg ∈ set_remove x s2 by right; apply set_remove_iff.
Qed.

Lemma set_eq_remove_union_not_elem_of  `{EqDecision A} : forall x (s1 s2 : list A),
  NoDup s1 ->
  NoDup s2 ->
  x ∉ s1 ->
  set_eq (set_union s1 (set_remove x s2)) (set_remove x (set_union s1 s2)).A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → x ∉ s1
      → set_eq (set_union s1 (set_remove x s2))
          (set_remove x (set_union s1 s2))
Proof.A: Type
EqDecision0: EqDecision A
∀ (x : A) (s1 s2 : list A),
  NoDup s1
  → NoDup s2
    → x ∉ s1
      → set_eq (set_union s1 (set_remove x s2))
          (set_remove x (set_union s1 s2))
  intros.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
set_eq (set_union s1 (set_remove x s2))
  (set_remove x (set_union s1 s2))
  assert (HnodupUs1s2 := H0).A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup s2
set_eq (set_union s1 (set_remove x s2))
  (set_remove x (set_union s1 s2))
  apply (set_union_nodup _ _ H) in HnodupUs1s2.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
set_eq (set_union s1 (set_remove x s2))
  (set_remove x (set_union s1 s2))
  split; intros msg Hin.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
Hin: msg ∈ set_union s1 (set_remove x s2)
msg ∈ set_remove x (set_union s1 s2)
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
Hin: msg ∈ set_remove x (set_union s1 s2)
msg ∈ set_union s1 (set_remove x s2)
  -A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
Hin: msg ∈ set_union s1 (set_remove x s2)
msg ∈ set_remove x (set_union s1 s2) apply set_remove_iff; [done |].A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
Hin: msg ∈ set_union s1 (set_remove x s2)
msg ∈ set_union s1 s2 ∧ msg ≠ x
    apply set_union_iff in Hin as []; split.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ s1
msg ∈ set_union s1 s2
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ s1
msg ≠ x
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ set_remove x s2
msg ∈ set_union s1 s2
A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ set_remove x s2
msg ≠ x
    +A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ s1
msg ∈ set_union s1 s2 by apply set_union_iff; left.
    +A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ s1
msg ≠ x by intro; subst; apply H1.
    +A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ set_remove x s2
msg ∈ set_union s1 s2 apply set_remove_iff in H2 as []; [| done].A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ s2
H3: msg ≠ x
msg ∈ set_union s1 s2
      by apply set_union_iff; right.
    +A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ set_remove x s2
msg ≠ x intro; subst.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
H2: x ∈ set_remove x s2
False
      by apply set_remove_iff in H2; itauto.
  -A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
Hin: msg ∈ set_remove x (set_union s1 s2)
msg ∈ set_union s1 (set_remove x s2) apply set_union_iff.A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
Hin: msg ∈ set_remove x (set_union s1 s2)
msg ∈ s1 ∨ msg ∈ set_remove x s2
    apply set_remove_iff in Hin as []; [| done].A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ set_union s1 s2
H3: msg ≠ x
msg ∈ s1 ∨ msg ∈ set_remove x s2
    apply set_union_iff in H2 as []; [by left |].A: Type
EqDecision0: EqDecision A
x: A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
H1: x ∉ s1
HnodupUs1s2: NoDup (set_union s1 s2)
msg: A
H2: msg ∈ s2
H3: msg ≠ x
msg ∈ s1 ∨ msg ∈ set_remove x s2
    by right; apply set_remove_iff.
Qed.

Lemma diff_app_nodup `{EqDecision A} : forall (s1 s2 : list A),
  NoDup s1 ->
  NoDup s2 ->
  NoDup (set_diff s1 s2 ++ s2).A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A,
  NoDup s1 → NoDup s2 → NoDup (set_diff s1 s2 ++ s2)
Proof.A: Type
EqDecision0: EqDecision A
∀ s1 s2 : list A,
  NoDup s1 → NoDup s2 → NoDup (set_diff s1 s2 ++ s2)
  intros.A: Type
EqDecision0: EqDecision A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
NoDup (set_diff s1 s2 ++ s2)
  apply NoDup_app; split_and!; [| | done].A: Type
EqDecision0: EqDecision A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
NoDup (set_diff s1 s2)
A: Type
EqDecision0: EqDecision A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
∀ x : A, x ∈ set_diff s1 s2 → x ∉ s2
  -A: Type
EqDecision0: EqDecision A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
NoDup (set_diff s1 s2) by apply set_diff_nodup.
  -A: Type
EqDecision0: EqDecision A
s1, s2: list A
H: NoDup s1
H0: NoDup s2
∀ x : A, x ∈ set_diff s1 s2 → x ∉ s2 by intros a; apply (set_diff_elim2 a s1).
Qed.

Lemma add_remove_inverse `{EqDecision X} :
  forall (lv : list X) (v : X),
    v ∉ lv ->
    set_remove v (set_add v lv) = lv.X: Type
EqDecision0: EqDecision X
∀ (lv : list X) (v : X),
  v ∉ lv → set_remove v (set_add v lv) = lv
Proof.X: Type
EqDecision0: EqDecision X
∀ (lv : list X) (v : X),
  v ∉ lv → set_remove v (set_add v lv) = lv
  induction lv as [| hd tl IHlv]; cbn; intros.X: Type
EqDecision0: EqDecision X
v: X
H: v ∉ []
(if decide (v = v) then [] else v :: empty_set) = []
X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHlv: ∀ v : X,
  v ∉ tl → set_remove v (set_add v tl) = tl
v: X
H: v ∉ hd :: tl
set_remove v
  (if decide (v = hd)
   then hd :: tl
   else hd :: set_add v tl) = 
hd :: tl
  -X: Type
EqDecision0: EqDecision X
v: X
H: v ∉ []
(if decide (v = v) then [] else v :: empty_set) = [] by rewrite decide_True.
  -X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHlv: ∀ v : X,
  v ∉ tl → set_remove v (set_add v tl) = tl
v: X
H: v ∉ hd :: tl
set_remove v
  (if decide (v = hd)
   then hd :: tl
   else hd :: set_add v tl) = 
hd :: tl rewrite elem_of_cons in H.X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHlv: ∀ v : X,
  v ∉ tl → set_remove v (set_add v tl) = tl
v: X
H: ¬ (v = hd ∨ v ∈ tl)
set_remove v
  (if decide (v = hd)
   then hd :: tl
   else hd :: set_add v tl) = 
hd :: tl
    destruct (decide (v = hd)) eqn: Heq; subst; cbn; [by itauto |].X: Type
EqDecision0: EqDecision X
hd: X
tl: list X
IHlv: ∀ v : X,
  v ∉ tl → set_remove v (set_add v tl) = tl
v: X
H: ¬ (v = hd ∨ v ∈ tl)
n: v ≠ hd
Heq: decide (v = hd) = right n
(if decide (v = hd)
 then set_add v tl
 else hd :: set_remove v (set_add v tl)) = 
hd :: tl
    by rewrite Heq, IHlv; itauto.
Qed.

Lemma set_union_iterated_empty `{EqDecision A} :
  forall ss : list (set A),
    (forall s : list A, s ∈ ss -> s = []) -> fold_right set_union [] ss = [].A: Type
EqDecision0: EqDecision A
∀ ss : list (set A),
  (∀ s : list A, s ∈ ss → s = [])
  → foldr set_union [] ss = []
Proof.A: Type
EqDecision0: EqDecision A
∀ ss : list (set A),
  (∀ s : list A, s ∈ ss → s = [])
  → foldr set_union [] ss = []
  induction ss; [done |]; cbn; intros H.A: Type
EqDecision0: EqDecision A
a: set A
ss: list (set A)
IHss: (∀ s : list A, s ∈ ss → s = [])
→ foldr set_union [] ss = []
H: ∀ s : list A, s ∈ a :: ss → s = []
set_union a (foldr set_union [] ss) = []
  rewrite IHss; cycle 1.A: Type
EqDecision0: EqDecision A
a: set A
ss: list (set A)
IHss: (∀ s : list A, s ∈ ss → s = [])
→ foldr set_union [] ss = []
H: ∀ s : list A, s ∈ a :: ss → s = []
∀ s : list A, s ∈ ss → s = []
A: Type
EqDecision0: EqDecision A
a: set A
ss: list (set A)
IHss: (∀ s : list A, s ∈ ss → s = [])
→ foldr set_union [] ss = []
H: ∀ s : list A, s ∈ a :: ss → s = []
set_union a [] = []
  -A: Type
EqDecision0: EqDecision A
a: set A
ss: list (set A)
IHss: (∀ s : list A, s ∈ ss → s = [])
→ foldr set_union [] ss = []
H: ∀ s : list A, s ∈ a :: ss → s = []
∀ s : list A, s ∈ ss → s = [] by intros s Hel; apply H; right.
  -A: Type
EqDecision0: EqDecision A
a: set A
ss: list (set A)
IHss: (∀ s : list A, s ∈ ss → s = [])
→ foldr set_union [] ss = []
H: ∀ s : list A, s ∈ a :: ss → s = []
set_union a [] = [] by cbn; apply H; left.
Qed.

For each element X of l1, exactly one occurrence of X is removed from l2. If no such occurrence exists, nothing happens.

Definition set_remove_list `{EqDecision A} (l1 l2 : list A) : list A :=
  fold_right set_remove l2 l1.

Example set_remove_list1 : set_remove_list [3; 1; 3] [1; 1; 2; 3; 3; 3; 3] = [1; 2; 3; 3].set_remove_list [3; 1; 3] [1; 1; 2; 3; 3; 3; 3] =
[1; 2; 3; 3]
Proof.set_remove_list [3; 1; 3] [1; 1; 2; 3; 3; 3; 3] =
[1; 2; 3; 3] done. Qed.

Example set_remove_list2 : set_remove_list [4] [1; 2; 3] = [1; 2; 3].set_remove_list [4] [1; 2; 3] = [1; 2; 3]
Proof.set_remove_list [4] [1; 2; 3] = [1; 2; 3] done. Qed.

Lemma set_remove_list_1
  `{EqDecision A}
  (a : A)
  (l1 l2 : list A)
  (Hin : a ∈ set_remove_list l1 l2) :
  a ∈ l2.A: Type
EqDecision0: EqDecision A
a: A
l1, l2: list A
Hin: a ∈ set_remove_list l1 l2
a ∈ l2
Proof.A: Type
EqDecision0: EqDecision A
a: A
l1, l2: list A
Hin: a ∈ set_remove_list l1 l2
a ∈ l2
  unfold set_remove_list in Hin.A: Type
EqDecision0: EqDecision A
a: A
l1, l2: list A
Hin: a ∈ foldr set_remove l2 l1
a ∈ l2
  induction l1.A: Type
EqDecision0: EqDecision A
a: A
l2: list A
Hin: a ∈ foldr set_remove l2 []
a ∈ l2
A: Type
EqDecision0: EqDecision A
a, a0: A
l1, l2: list A
Hin: a ∈ foldr set_remove l2 (a0 :: l1)
IHl1: a ∈ foldr set_remove l2 l1 → a ∈ l2
a ∈ l2
  -A: Type
EqDecision0: EqDecision A
a: A
l2: list A
Hin: a ∈ foldr set_remove l2 []
a ∈ l2 by simpl in Hin; itauto.
  -A: Type
EqDecision0: EqDecision A
a, a0: A
l1, l2: list A
Hin: a ∈ foldr set_remove l2 (a0 :: l1)
IHl1: a ∈ foldr set_remove l2 l1 → a ∈ l2
a ∈ l2 by simpl in Hin; apply set_remove_1, IHl1 in Hin.
Qed.

Lemma set_prod_nodup `(s1 : set A) `(s2 : set B) :
  NoDup s1 ->
  NoDup s2 ->
  NoDup (set_prod s1 s2).A: Type
s1: set A
B: Type
s2: set B
NoDup s1 → NoDup s2 → NoDup (set_prod s1 s2)
Proof.A: Type
s1: set A
B: Type
s2: set B
NoDup s1 → NoDup s2 → NoDup (set_prod s1 s2)
  intros Hs1 H22; induction Hs1; cbn; [by constructor |].A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
NoDup (map (λ y : B, (x, y)) s2 ++ set_prod l s2)
  apply NoDup_app; split_and!; [| | done].A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
NoDup (map (λ y : B, (x, y)) s2)
A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
∀ x0 : A * B,
  x0 ∈ map (λ y : B, (x, y)) s2 → x0 ∉ set_prod l s2
  -A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
NoDup (map (λ y : B, (x, y)) s2) by apply NoDup_fmap; [congruence |].
  -A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
∀ x0 : A * B,
  x0 ∈ map (λ y : B, (x, y)) s2 → x0 ∉ set_prod l s2 intros [a b].A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
a: A
b: B
(a, b) ∈ map (λ y : B, (x, y)) s2
→ (a, b) ∉ set_prod l s2
    rewrite elem_of_list_fmap, elem_of_list_prod.A, B: Type
s2: set B
x: A
l: list A
H: x ∉ l
Hs1: NoDup l
H22: NoDup s2
IHHs1: NoDup (set_prod l s2)
a: A
b: B
(∃ y : B, (a, b) = (x, y) ∧ y ∈ s2)
→ ¬ (a ∈ l ∧ b ∈ s2)
    by intros [_ [[= -> _] _]] [].
Qed.

An alternative to set_diff. Unlike set_diff, the result may contain duplicates if the first argument list l does.

This definition exists to make proving len_set_diff_decrease more convenient, because length of filter can be simplified step by step while doing induction over l.

Definition set_diff_filter `{EqDecision A} (l r : list A) :=
  filter (.∉ r) l.

The characteristic membership property, parallel to set_diff_iff.

Lemma set_diff_filter_iff `{EqDecision A} (a : A) l r :
  a ∈ set_diff_filter l r <-> a ∈ l /\ a ∉ r.A: Type
EqDecision0: EqDecision A
a: A
l, r: list A
a ∈ set_diff_filter l r ↔ a ∈ l ∧ a ∉ r
Proof.A: Type
EqDecision0: EqDecision A
a: A
l, r: list A
a ∈ set_diff_filter l r ↔ a ∈ l ∧ a ∉ r
  induction l; simpl.A: Type
EqDecision0: EqDecision A
a: A
r: list A
a ∈ set_diff_filter [] r ↔ a ∈ [] ∧ a ∉ r
A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ set_diff_filter l r ↔ a ∈ l ∧ a ∉ r
a ∈ set_diff_filter (a0 :: l) r ↔ a ∈ a0 :: l ∧ a ∉ r
  -A: Type
EqDecision0: EqDecision A
a: A
r: list A
a ∈ set_diff_filter [] r ↔ a ∈ [] ∧ a ∉ r by cbn; split; intros; [inversion H | itauto].
  -A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ set_diff_filter l r ↔ a ∈ l ∧ a ∉ r
a ∈ set_diff_filter (a0 :: l) r ↔ a ∈ a0 :: l ∧ a ∉ r unfold set_diff_filter in *.A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
a ∈ filter (λ x : A, x ∉ r) (a0 :: l)
↔ a ∈ a0 :: l ∧ a ∉ r
    rewrite filter_cons.A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
a
∈ (if decide (a0 ∉ r)
   then a0 :: filter (λ x : A, x ∉ r) l
   else filter (λ x : A, x ∉ r) l)
↔ a ∈ a0 :: l ∧ a ∉ r
    destruct (decide (a0 ∉ r)).A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
n: a0 ∉ r
a ∈ a0 :: filter (λ x : A, x ∉ r) l
↔ a ∈ a0 :: l ∧ a ∉ r
A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
n: ¬ (a0 ∉ r)
a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ a0 :: l ∧ a ∉ r
    +A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
n: a0 ∉ r
a ∈ a0 :: filter (λ x : A, x ∉ r) l
↔ a ∈ a0 :: l ∧ a ∉ r rewrite 2 elem_of_cons, IHl.A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
n: a0 ∉ r
a = a0 ∨ a ∈ l ∧ a ∉ r ↔ (a = a0 ∨ a ∈ l) ∧ a ∉ r
      by split; itauto congruence.
    +A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
n: ¬ (a0 ∉ r)
a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ a0 :: l ∧ a ∉ r rewrite elem_of_cons.A: Type
EqDecision0: EqDecision A
a, a0: A
l, r: list A
IHl: a ∈ filter (λ x : A, x ∉ r) l ↔ a ∈ l ∧ a ∉ r
n: ¬ (a0 ∉ r)
a ∈ filter (λ x : A, x ∉ r) l
↔ (a = a0 ∨ a ∈ l) ∧ a ∉ r
      by split; itauto congruence.
Qed.

Lemma set_diff_filter_nodup `{EqDecision A} (l r : list A) :
  NoDup l -> NoDup (set_diff_filter l r).A: Type
EqDecision0: EqDecision A
l, r: list A
NoDup l → NoDup (set_diff_filter l r)
Proof.A: Type
EqDecision0: EqDecision A
l, r: list A
NoDup l → NoDup (set_diff_filter l r)
  by intros H; apply NoDup_filter.
Qed.

Prove that subtracting a superset cannot produce a smaller result. This lemma is used to prove len_set_diff_decrease.

Lemma len_set_diff_incl_le `{EqDecision A} (l a b : list A)
      (H_subseteq : forall x, x ∈ b -> x ∈ a) :
  length (set_diff_filter l a) <= length (set_diff_filter l b).A: Type
EqDecision0: EqDecision A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
length (set_diff_filter l a)
≤ length (set_diff_filter l b)
Proof.A: Type
EqDecision0: EqDecision A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
length (set_diff_filter l a)
≤ length (set_diff_filter l b)
  induction l; [done |].A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
length (set_diff_filter (a0 :: l) a)
≤ length (set_diff_filter (a0 :: l) b)
  unfold set_diff_filter.A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
length (filter (λ x : A, x ∉ a) (a0 :: l))
≤ length (filter (λ x : A, x ∉ b) (a0 :: l))
  rewrite 2 filter_cons.A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
length
  (if decide (a0 ∉ a)
   then a0 :: filter (λ x : A, x ∉ a) l
   else filter (λ x : A, x ∉ a) l)
≤ length
    (if decide (a0 ∉ b)
     then a0 :: filter (λ x : A, x ∉ b) l
     else filter (λ x : A, x ∉ b) l)
  destruct (decide (a0 ∉ a)); destruct (decide (a0 ∉ b)).A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: a0 ∉ a
n0: a0 ∉ b
length (a0 :: filter (λ x : A, x ∉ a) l)
≤ length (a0 :: filter (λ x : A, x ∉ b) l)
A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: a0 ∉ a
n0: ¬ (a0 ∉ b)
length (a0 :: filter (λ x : A, x ∉ a) l)
≤ length (filter (λ x : A, x ∉ b) l)
A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l)
≤ length (a0 :: filter (λ x : A, x ∉ b) l)
A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: ¬ (a0 ∉ b)
length (filter (λ x : A, x ∉ a) l)
≤ length (filter (λ x : A, x ∉ b) l)
  -A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: a0 ∉ a
n0: a0 ∉ b
length (a0 :: filter (λ x : A, x ∉ a) l)
≤ length (a0 :: filter (λ x : A, x ∉ b) l) by simpl; unfold set_diff_filter in IHl; lia.
  -A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: a0 ∉ a
n0: ¬ (a0 ∉ b)
length (a0 :: filter (λ x : A, x ∉ a) l)
≤ length (filter (λ x : A, x ∉ b) l) by itauto.
  -A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l)
≤ length (a0 :: filter (λ x : A, x ∉ b) l) by simpl; apply le_S, IHl.
  -A: Type
EqDecision0: EqDecision A
a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
IHl: length (set_diff_filter l a)
≤ length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: ¬ (a0 ∉ b)
length (filter (λ x : A, x ∉ a) l)
≤ length (filter (λ x : A, x ∉ b) l) by apply IHl.
Qed.

Prove that strictly increasing the set to be subtracted, by adding an element actually found in l will decrease the size of the result.

Lemma len_set_diff_decrease `{EqDecision A} (new : A) (l a b : list A)
      (H_subseteq : forall x, x ∈ b -> x ∈ a)
      (H_new_is_new : new ∈ a /\ new ∉ b)
      (H_new_is_relevant : new ∈ l) :
  length (set_diff_filter l a) < length (set_diff_filter l b).A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
H_new_is_relevant: new ∈ l
length (set_diff_filter l a) <
length (set_diff_filter l b)
Proof.A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
H_new_is_relevant: new ∈ l
length (set_diff_filter l a) <
length (set_diff_filter l b)
  induction l; [by inversion H_new_is_relevant |];
    apply elem_of_cons in H_new_is_relevant; destruct H_new_is_relevant.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
H: new = a0
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length (set_diff_filter (a0 :: l) a) <
length (set_diff_filter (a0 :: l) b)
A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
H: new ∈ l
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length (set_diff_filter (a0 :: l) a) <
length (set_diff_filter (a0 :: l) b)
  -A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
H: new = a0
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length (set_diff_filter (a0 :: l) a) <
length (set_diff_filter (a0 :: l) b) subst a0.A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length (set_diff_filter (new :: l) a) <
length (set_diff_filter (new :: l) b)
    unfold set_diff_filter.A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length (filter (λ x : A, x ∉ a) (new :: l)) <
length (filter (λ x : A, x ∉ b) (new :: l))
    rewrite 2 filter_cons.A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length
  (if decide (new ∉ a)
   then new :: filter (λ x : A, x ∉ a) l
   else filter (λ x : A, x ∉ a) l) <
length
  (if decide (new ∉ b)
   then new :: filter (λ x : A, x ∉ b) l
   else filter (λ x : A, x ∉ b) l)
    destruct (decide (new ∉ a)); [by itauto |].A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
n: ¬ (new ∉ a)
length (filter (λ x : A, x ∉ a) l) <
length
  (if decide (new ∉ b)
   then new :: filter (λ x : A, x ∉ b) l
   else filter (λ x : A, x ∉ b) l)
    destruct (decide (new ∉ b)); [| by contradict n0; itauto].A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
n: ¬ (new ∉ a)
n0: new ∉ b
length (filter (λ x : A, x ∉ a) l) <
length (new :: filter (λ x : A, x ∉ b) l)
    simpl.A: Type
EqDecision0: EqDecision A
new: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
n: ¬ (new ∉ a)
n0: new ∉ b
length (filter (λ x : A, x ∉ a) l) <
S (length (filter (λ x : A, x ∉ b) l))
    by apply le_n_S, len_set_diff_incl_le.
  -A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
H: new ∈ l
IHl: new ∈ l
→ length (set_diff_filter l a) <
  length (set_diff_filter l b)
length (set_diff_filter (a0 :: l) a) <
length (set_diff_filter (a0 :: l) b) specialize (IHl H); clear H.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
length (set_diff_filter (a0 :: l) a) <
length (set_diff_filter (a0 :: l) b)
    unfold set_diff_filter.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
length (filter (λ x : A, x ∉ a) (a0 :: l)) <
length (filter (λ x : A, x ∉ b) (a0 :: l))
    rewrite 2 filter_cons.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
length
  (if decide (a0 ∉ a)
   then a0 :: filter (λ x : A, x ∉ a) l
   else filter (λ x : A, x ∉ a) l) <
length
  (if decide (a0 ∉ b)
   then a0 :: filter (λ x : A, x ∉ b) l
   else filter (λ x : A, x ∉ b) l)
    destruct (decide (a0 ∉ a)); destruct (decide (a0 ∉ b)).A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: a0 ∉ a
n0: a0 ∉ b
length (a0 :: filter (λ x : A, x ∉ a) l) <
length (a0 :: filter (λ x : A, x ∉ b) l)
A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: a0 ∉ a
n0: ¬ (a0 ∉ b)
length (a0 :: filter (λ x : A, x ∉ a) l) <
length (filter (λ x : A, x ∉ b) l)
A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l) <
length (a0 :: filter (λ x : A, x ∉ b) l)
A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: ¬ (a0 ∉ b)
length (filter (λ x : A, x ∉ a) l) <
length (filter (λ x : A, x ∉ b) l)
    +A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: a0 ∉ a
n0: a0 ∉ b
length (a0 :: filter (λ x : A, x ∉ a) l) <
length (a0 :: filter (λ x : A, x ∉ b) l) simpl.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: a0 ∉ a
n0: a0 ∉ b
S (length (filter (λ x : A, x ∉ a) l)) <
S (length (filter (λ x : A, x ∉ b) l))
      rewrite <- Nat.succ_lt_mono.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: a0 ∉ a
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l) <
length (filter (λ x : A, x ∉ b) l)
      by apply IHl.
    +A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: a0 ∉ a
n0: ¬ (a0 ∉ b)
length (a0 :: filter (λ x : A, x ∉ a) l) <
length (filter (λ x : A, x ∉ b) l) contradict n.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n0: ¬ (a0 ∉ b)
a0 ∈ a
      apply H_subseteq.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n0: ¬ (a0 ∉ b)
a0 ∈ b
      by destruct (decide (a0 ∈ b)).
    +A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l) <
length (a0 :: filter (λ x : A, x ∉ b) l) simpl.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l) <
S (length (filter (λ x : A, x ∉ b) l))
      apply Nat.lt_lt_succ_r.A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: a0 ∉ b
length (filter (λ x : A, x ∉ a) l) <
length (filter (λ x : A, x ∉ b) l)
      by apply IHl.
    +A: Type
EqDecision0: EqDecision A
new, a0: A
l, a, b: list A
H_subseteq: ∀ x : A, x ∈ b → x ∈ a
H_new_is_new: new ∈ a ∧ new ∉ b
IHl: length (set_diff_filter l a) <
length (set_diff_filter l b)
n: ¬ (a0 ∉ a)
n0: ¬ (a0 ∉ b)
length (filter (λ x : A, x ∉ a) l) <
length (filter (λ x : A, x ∉ b) l) by apply IHl.
Qed.

Lemma len_set_diff_map_set_add `{EqDecision B} (new : B) `{EqDecision A} (f : B -> A)
      (a : list B) (l : list A)
      (H_new_is_new : f new ∉ map f a)
      (H_new_is_relevant : f new ∈ l) :
  length (set_diff_filter l (map f (set_add new a))) <
    length (set_diff_filter l (map f a)).B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
length (set_diff_filter l (map f (set_add new a))) <
length (set_diff_filter l (map f a))
Proof.B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
length (set_diff_filter l (map f (set_add new a))) <
length (set_diff_filter l (map f a))
  apply len_set_diff_decrease with (f new); [.. | done].B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
∀ x : A, x ∈ map f a → x ∈ map f (set_add new a)
B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
f new ∈ map f (set_add new a) ∧ f new ∉ map f a
  -B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
∀ x : A, x ∈ map f a → x ∈ map f (set_add new a) intro x.B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
x: A
x ∈ map f a → x ∈ map f (set_add new a) rewrite 2 elem_of_list_fmap.B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
x: A
(∃ y : B, x = f y ∧ y ∈ a)
→ ∃ y : B, x = f y ∧ y ∈ set_add new a
    intros [x0 [Hx0 Hin]].B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
x: A
x0: B
Hx0: x = f x0
Hin: x0 ∈ a
∃ y : B, x = f y ∧ y ∈ set_add new a exists x0.B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
x: A
x0: B
Hx0: x = f x0
Hin: x0 ∈ a
x = f x0 ∧ x0 ∈ set_add new a
    by rewrite set_add_iff; itauto.
  -B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
f new ∈ map f (set_add new a) ∧ f new ∉ map f a split; [| done].B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
f new ∈ map f (set_add new a)
    apply elem_of_list_fmap_1.B: Type
EqDecision0: EqDecision B
new: B
A: Type
EqDecision1: EqDecision A
f: B → A
a: list B
l: list A
H_new_is_new: f new ∉ map f a
H_new_is_relevant: f new ∈ l
new ∈ set_add new a
    by apply set_add_iff; left.
Qed.

#[export] Instance set_eq_elem_of (A : Type) :
  Proper (@eq A ==> @set_eq A ==> iff) elem_of_list.A: Type
Proper (eq ==> set_eq ==> iff) elem_of_list
Proof.A: Type
Proper (eq ==> set_eq ==> iff) elem_of_list
  by intros x y -> l1 l2 H; split; apply H.
Qed.

#[export] Instance set_elem_of_subseteq (A : Type) :
  Proper (@eq A ==> @list_subseteq A ==> impl) elem_of_list.A: Type
Proper (eq ==> list_subseteq ==> impl) elem_of_list
Proof.A: Type
Proper (eq ==> list_subseteq ==> impl) elem_of_list by intros x y -> l1 l2 H; firstorder. Qed.

Lemma set_union_iterated_preserves_prop
  `{EqDecision A}
  (ss : list (set A))
  (P : A -> Prop)
  (Hp : forall (s : set A), forall (a : A), (s ∈ ss /\ a ∈ s) -> P a) :
  forall (a : A), a ∈ fold_right set_union [] ss -> P a.A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
∀ a : A, a ∈ foldr set_union [] ss → P a
Proof.A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
∀ a : A, a ∈ foldr set_union [] ss → P a
  intros.A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
a: A
H: a ∈ foldr set_union [] ss
P a
  apply set_union_in_iterated in H.A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
a: A
H: Exists (λ s : set A, a ∈ s) ss
P a rewrite Exists_exists in H.A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
a: A
H: ∃ x : set A, x ∈ ss ∧ a ∈ x
P a
  destruct H as [s [Hins Hina]].A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
a: A
s: set A
Hins: s ∈ ss
Hina: a ∈ s
P a
  apply Hp with (s := s).A: Type
EqDecision0: EqDecision A
ss: list (set A)
P: A → Prop
Hp: ∀ (s : set A) (a : A), s ∈ ss ∧ a ∈ s → P a
a: A
s: set A
Hins: s ∈ ss
Hina: a ∈ s
s ∈ ss ∧ a ∈ s
  by itauto.
Qed.

Lemma filter_set_eq {X} P Q
 `{forall (x : X), Decision (P x)} `{forall (x : X), Decision (Q x)}
   (l : list X)
   (resf := filter P l)
   (resg := filter Q l) :
   set_eq resf resg -> resf = resg.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
set_eq resf resg → resf = resg
Proof.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
set_eq resf resg → resf = resg
  intros.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
H1: set_eq resf resg
resf = resg
  unfold resf, resg in *.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
H1: set_eq (filter P l) (filter Q l)
filter P l = filter Q l
  apply filter_ext_elem_of.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
H1: set_eq (filter P l) (filter Q l)
∀ a : X, a ∈ l → P a ↔ Q a intros.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
H1: set_eq (filter P l) (filter Q l)
a: X
H2: a ∈ l
P a ↔ Q a
  unfold set_eq in H1.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
H1: filter P l ⊆ filter Q l ⊆ filter P l
a: X
H2: a ∈ l
P a ↔ Q a
  destruct H1 as [H1 H1'].X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
H1: filter P l ⊆ filter Q l
H1': filter Q l ⊆ filter P l
a: X
H2: a ∈ l
P a ↔ Q a
  specialize (H1 a).X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
a: X
H1: a ∈ filter P l → a ∈ filter Q l
H1': filter Q l ⊆ filter P l
H2: a ∈ l
P a ↔ Q a specialize (H1' a).X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
a: X
H1: a ∈ filter P l → a ∈ filter Q l
H1': a ∈ filter Q l → a ∈ filter P l
H2: a ∈ l
P a ↔ Q a
  split; intros.X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
a: X
H1: a ∈ filter P l → a ∈ filter Q l
H1': a ∈ filter Q l → a ∈ filter P l
H2: a ∈ l
H3: P a
Q a
X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
a: X
H1: a ∈ filter P l → a ∈ filter Q l
H1': a ∈ filter Q l → a ∈ filter P l
H2: a ∈ l
H3: Q a
P a
  -X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
a: X
H1: a ∈ filter P l → a ∈ filter Q l
H1': a ∈ filter Q l → a ∈ filter P l
H2: a ∈ l
H3: P a
Q a by eapply elem_of_list_filter, H1, elem_of_list_filter.
  -X: Type
P, Q: X → Prop
H: ∀ x : X, Decision (P x)
H0: ∀ x : X, Decision (Q x)
l: list X
resf:= filter P l: list X
resg:= filter Q l: list X
a: X
H1: a ∈ filter P l → a ∈ filter Q l
H1': a ∈ filter Q l → a ∈ filter P l
H2: a ∈ l
H3: Q a
P a by eapply elem_of_list_filter, H1', elem_of_list_filter.
Qed.

Lemma subseteq_appr : forall A (l m n : list A), l ⊆ n -> l ⊆ m ++ n.∀ (A : Type) (l m n : list A), l ⊆ n → l ⊆ m ++ n
Proof.∀ (A : Type) (l m n : list A), l ⊆ n → l ⊆ m ++ n
  intros A l m n x y yinl.A: Type
l, m, n: list A
x: l ⊆ n
y: A
yinl: y ∈ l
y ∈ m ++ n
  apply x in yinl.A: Type
l, m, n: list A
x: l ⊆ n
y: A
yinl: y ∈ n
y ∈ m ++ n
  by apply elem_of_app; right.
Qed.

Lemma elem_of_union_fold
  `{EqDecision A}
  (haystack : list (list A))
  (a : A) :
  a ∈ fold_right set_union [] haystack
  <->
  exists (needle : list A), a ∈ needle /\ needle ∈ haystack.A: Type
EqDecision0: EqDecision A
haystack: list (list A)
a: A
a ∈ foldr set_union [] haystack
↔ (∃ needle : list A, a ∈ needle ∧ needle ∈ haystack)
Proof.A: Type
EqDecision0: EqDecision A
haystack: list (list A)
a: A
a ∈ foldr set_union [] haystack
↔ (∃ needle : list A, a ∈ needle ∧ needle ∈ haystack)
  split.A: Type
EqDecision0: EqDecision A
haystack: list (list A)
a: A
a ∈ foldr set_union [] haystack
→ ∃ needle : list A, a ∈ needle ∧ needle ∈ haystack
A: Type
EqDecision0: EqDecision A
haystack: list (list A)
a: A
(∃ needle : list A, a ∈ needle ∧ needle ∈ haystack)
→ a ∈ foldr set_union [] haystack
  -A: Type
EqDecision0: EqDecision A
haystack: list (list A)
a: A
a ∈ foldr set_union [] haystack
→ ∃ needle : list A, a ∈ needle ∧ needle ∈ haystack generalize dependent a.A: Type
EqDecision0: EqDecision A
haystack: list (list A)
∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A, a ∈ needle ∧ needle ∈ haystack
    generalize dependent haystack.A: Type
EqDecision0: EqDecision A
∀ (haystack : list (list A)) (a : A),
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A, a ∈ needle ∧ needle ∈ haystack
    induction haystack.A: Type
EqDecision0: EqDecision A
∀ a : A,
  a ∈ foldr set_union [] []
  → ∃ needle : list A, a ∈ needle ∧ needle ∈ []
A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
∀ a0 : A,
  a0 ∈ foldr set_union [] (a :: haystack)
  → ∃ needle : list A,
      a0 ∈ needle ∧ needle ∈ a :: haystack
    +A: Type
EqDecision0: EqDecision A
∀ a : A,
  a ∈ foldr set_union [] []
  → ∃ needle : list A, a ∈ needle ∧ needle ∈ [] by intros; cbn in H; inversion H.
    +A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
∀ a0 : A,
  a0 ∈ foldr set_union [] (a :: haystack)
  → ∃ needle : list A,
      a0 ∈ needle ∧ needle ∈ a :: haystack intros.A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0 ∈ foldr set_union [] (a :: haystack)
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack
      unfold fold_right in H.A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0
∈ set_union a
    ((fix fold_right (l : list (set A)) : set A :=
        match l with
        | [] => []
        | b :: t => set_union b (fold_right t)
        end) haystack)
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack
      rewrite set_union_iff in H.A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0 ∈ a
∨ a0
  ∈ (fix fold_right (l : list (set A)) : set A :=
       match l with
       | [] => []
       | b :: t => set_union b (fold_right t)
       end) haystack
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack
      destruct H.A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0 ∈ a
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack
A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0
∈ (fix fold_right (l : list (set A)) : set A :=
     match l with
     | [] => []
     | b :: t => set_union b (fold_right t)
     end) haystack
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack
      *A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0 ∈ a
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack by setoid_rewrite elem_of_cons; eauto.
      *A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0
∈ (fix fold_right (l : list (set A)) : set A :=
     match l with
     | [] => []
     | b :: t => set_union b (fold_right t)
     end) haystack
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack destruct (IHhaystack a0 H) as (needle & Hin1 & Hin2).A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  a ∈ foldr set_union [] haystack
  → ∃ needle : list A,
      a ∈ needle ∧ needle ∈ haystack
a0: A
H: a0
∈ (fix fold_right (l : list (set A)) : set A :=
     match l with
     | [] => []
     | b :: t => set_union b (fold_right t)
     end) haystack
needle: list A
Hin1: a0 ∈ needle
Hin2: needle ∈ haystack
∃ needle : list A,
  a0 ∈ needle ∧ needle ∈ a :: haystack
        by setoid_rewrite elem_of_cons; eauto.
   -A: Type
EqDecision0: EqDecision A
haystack: list (list A)
a: A
(∃ needle : list A, a ∈ needle ∧ needle ∈ haystack)
→ a ∈ foldr set_union [] haystack generalize dependent a.A: Type
EqDecision0: EqDecision A
haystack: list (list A)
∀ a : A,
  (∃ needle : list A, a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
     generalize dependent haystack.A: Type
EqDecision0: EqDecision A
∀ (haystack : list (list A)) (a : A),
  (∃ needle : list A, a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
     induction haystack.A: Type
EqDecision0: EqDecision A
∀ a : A,
  (∃ needle : list A, a ∈ needle ∧ needle ∈ [])
  → a ∈ foldr set_union [] []
A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
∀ a0 : A,
  (∃ needle : list A,
     a0 ∈ needle ∧ needle ∈ a :: haystack)
  → a0 ∈ foldr set_union [] (a :: haystack)
     +A: Type
EqDecision0: EqDecision A
∀ a : A,
  (∃ needle : list A, a ∈ needle ∧ needle ∈ [])
  → a ∈ foldr set_union [] [] by cbn; intros a (x & Ha & Hx); inversion Hx.
     +A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
∀ a0 : A,
  (∃ needle : list A,
     a0 ∈ needle ∧ needle ∈ a :: haystack)
  → a0 ∈ foldr set_union [] (a :: haystack) intros a0 (needle & Hin & Hin2).A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
Hin2: needle ∈ a :: haystack
a0 ∈ foldr set_union [] (a :: haystack)
       apply elem_of_cons in Hin2 as [<- |]; cbn.A: Type
EqDecision0: EqDecision A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
a0 ∈ set_union needle (foldr set_union [] haystack)
A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
H: needle ∈ haystack
a0 ∈ set_union a (foldr set_union [] haystack)
       *A: Type
EqDecision0: EqDecision A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
a0 ∈ set_union needle (foldr set_union [] haystack) by apply set_union_iff; auto.
       *A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
H: needle ∈ haystack
a0 ∈ set_union a (foldr set_union [] haystack) apply set_union_iff; right.A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
H: needle ∈ haystack
a0 ∈ foldr set_union [] haystack
         apply IHhaystack.A: Type
EqDecision0: EqDecision A
a: list A
haystack: list (list A)
IHhaystack: ∀ a : A,
  (∃ needle : list A,
     a ∈ needle ∧ needle ∈ haystack)
  → a ∈ foldr set_union [] haystack
a0: A
needle: list A
Hin: a0 ∈ needle
H: needle ∈ haystack
∃ needle : list A, a0 ∈ needle ∧ needle ∈ haystack
         by exists needle.
Qed.

Lemma subseteq_Forall (A : Type) (P : A -> Prop) (l1 l2 : list A) :
 l2 ⊆ l1 -> Forall P l1 -> Forall P l2.A: Type
P: A → Prop
l1, l2: list A
l2 ⊆ l1 → Forall P l1 → Forall P l2
Proof.A: Type
P: A → Prop
l1, l2: list A
l2 ⊆ l1 → Forall P l1 → Forall P l2
  intros Hsub Hfor.A: Type
P: A → Prop
l1, l2: list A
Hsub: l2 ⊆ l1
Hfor: Forall P l1
Forall P l2
  apply Forall_forall.A: Type
P: A → Prop
l1, l2: list A
Hsub: l2 ⊆ l1
Hfor: Forall P l1
∀ x : A, x ∈ l2 → P x
  rewrite Forall_forall in Hfor.A: Type
P: A → Prop
l1, l2: list A
Hsub: l2 ⊆ l1
Hfor: ∀ x : A, x ∈ l1 → P x
∀ x : A, x ∈ l2 → P x
  intros.A: Type
P: A → Prop
l1, l2: list A
Hsub: l2 ⊆ l1
Hfor: ∀ x : A, x ∈ l1 → P x
x: A
H: x ∈ l2
P x
  by apply Hfor, Hsub.
Qed.