Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Finite sets library

This module implements bridges (as functors) from dependent to/from non-dependent set signature.

Require Export FSetInterface.
Set Implicit Arguments.
Unset Strict Implicit.
Set Firstorder Depth 2.

From non-dependent signature S to dependent signature Sdep.

Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.

  Definition empty : {s : t | Empty s}.{s : t | Empty s}
  Proof.{s : t | Empty s}
    exists empty; auto with set.
  Qed.

  Definition is_empty : forall s : t, {Empty s} + {~ Empty s}.forall s : t, {Empty s} + {~ Empty s}
  Proof.forall s : t, {Empty s} + {~ Empty s}
    intros; generalize (is_empty_1 (s:=s)) (is_empty_2 (s:=s)).s:t
(Empty s -> is_empty s = true) ->
(is_empty s = true -> Empty s) ->
{Empty s} + {~ Empty s}
    case (is_empty s); intuition.
  Qed.


  Definition mem : forall (x : elt) (s : t), {In x s} + {~ In x s}.forall (x : elt) (s : t), {In x s} + {~ In x s}
  Proof.forall (x : elt) (s : t), {In x s} + {~ In x s}
    intros; generalize (mem_1 (s:=s) (x:=x)) (mem_2 (s:=s) (x:=x)).x:elt
s:t
(In x s -> mem x s = true) ->
(mem x s = true -> In x s) -> {In x s} + {~ In x s}
    case (mem x s); intuition.
  Qed.

  Definition Add (x : elt) (s s' : t) :=
    forall y : elt, In y s' <-> E.eq x y \/ In y s.

  Definition add : forall (x : elt) (s : t), {s' : t | Add x s s'}.forall (x : elt) (s : t), {s' : t | Add x s s'}
  Proof.forall (x : elt) (s : t), {s' : t | Add x s s'}
    intros; exists (add x s); auto.x:elt
s:t
Add x s (add x s)
    unfold Add; intuition.x:elt
s:t
y:elt
H:In y (add x s)
E.eq x y \/ In y s
    elim (E.eq_dec x y); auto.x:elt
s:t
y:elt
H:In y (add x s)
~ E.eq x y -> E.eq x y \/ In y s
    intros; right.x:elt
s:t
y:elt
H:In y (add x s)
b:~ E.eq x y
In y s
    eapply add_3; eauto.
  Qed.

  Definition singleton :
    forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}.forall x : elt,
{s : t | forall y : elt, In y s <-> E.eq x y}
  Proof.forall x : elt,
{s : t | forall y : elt, In y s <-> E.eq x y}
    intros; exists (singleton x); intuition.
  Qed.

  Definition remove :
    forall (x : elt) (s : t),
    {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}.forall (x : elt) (s : t),
{s' : t |
forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}
  Proof.forall (x : elt) (s : t),
{s' : t |
forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}
    intros; exists (remove x s); intuition.x:elt
s:t
y:elt
H:In y (remove x s)
H0:E.eq x y
False
x:elt
s:t
y:elt
H:In y (remove x s)
In y s
    absurd (In x (remove x s)); auto with set.x:elt
s:t
y:elt
H:In y (remove x s)
H0:E.eq x y
In x (remove x s)
x:elt
s:t
y:elt
H:In y (remove x s)
In y s
    apply In_1 with y; auto.x:elt
s:t
y:elt
H:In y (remove x s)
In y s
    elim (E.eq_dec x y); intros; auto.x:elt
s:t
y:elt
H:In y (remove x s)
a:E.eq x y
In y s
x:elt
s:t
y:elt
H:In y (remove x s)
b:~ E.eq x y
In y s
    absurd (In x (remove x s)); auto with set.x:elt
s:t
y:elt
H:In y (remove x s)
a:E.eq x y
In x (remove x s)
x:elt
s:t
y:elt
H:In y (remove x s)
b:~ E.eq x y
In y s
    apply In_1 with y; auto.x:elt
s:t
y:elt
H:In y (remove x s)
b:~ E.eq x y
In y s
    eauto with set.
  Qed.

  Definition union :
    forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s \/ In x s'}.forall s s' : t,
{s'' : t |
forall x : elt, In x s'' <-> In x s \/ In x s'}
  Proof.forall s s' : t,
{s'' : t |
forall x : elt, In x s'' <-> In x s \/ In x s'}
    intros; exists (union s s'); intuition.
  Qed.

  Definition inter :
    forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}.forall s s' : t,
{s'' : t |
forall x : elt, In x s'' <-> In x s /\ In x s'}
  Proof.forall s s' : t,
{s'' : t |
forall x : elt, In x s'' <-> In x s /\ In x s'}
    intros; exists (inter s s'); intuition; eauto with set.
  Qed.

  Definition diff :
    forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}.forall s s' : t,
{s'' : t |
forall x : elt, In x s'' <-> In x s /\ ~ In x s'}
  Proof.forall s s' : t,
{s'' : t |
forall x : elt, In x s'' <-> In x s /\ ~ In x s'}
    intros; exists (diff s s'); intuition; eauto with set.s, s':t
x:elt
H:In x (diff s s')
H0:In x s'
False
    absurd (In x s'); eauto with set.
  Qed.

  Definition equal : forall s s' : t, {Equal s s'} + {~ Equal s s'}.forall s s' : t, {s [=] s'} + {~ s [=] s'}
  Proof.forall s s' : t, {s [=] s'} + {~ s [=] s'}
    intros.s, s':t
{s [=] s'} + {~ s [=] s'}
    generalize (equal_1 (s:=s) (s':=s')) (equal_2 (s:=s) (s':=s')).s, s':t
(s [=] s' -> equal s s' = true) ->
(equal s s' = true -> s [=] s') ->
{s [=] s'} + {~ s [=] s'}
    case (equal s s'); intuition.
  Qed.

  Definition subset : forall s s' : t, {Subset s s'} + {~Subset s s'}.forall s s' : t, {s [<=] s'} + {~ s [<=] s'}
  Proof.forall s s' : t, {s [<=] s'} + {~ s [<=] s'}
    intros.s, s':t
{s [<=] s'} + {~ s [<=] s'}
    generalize (subset_1 (s:=s) (s':=s')) (subset_2 (s:=s) (s':=s')).s, s':t
(s [<=] s' -> subset s s' = true) ->
(subset s s' = true -> s [<=] s') ->
{s [<=] s'} + {~ s [<=] s'}
    case (subset s s'); intuition.
  Qed.

  Definition elements :
    forall s : t,
    {l : list elt | sort E.lt l /\ (forall x : elt, In x s <-> InA E.eq x l)}.forall s : t,
{l : list elt |
Sorted E.lt l /\
(forall x : elt, In x s <-> InA E.eq x l)}
   Proof.forall s : t,
{l : list elt |
Sorted E.lt l /\
(forall x : elt, In x s <-> InA E.eq x l)}
     intros; exists (elements s); intuition.
   Defined.

  Definition fold :
    forall (A : Type) (f : elt -> A -> A) (s : t) (i : A),
    {r : A |   let (l,_) := elements s in
                  r = fold_left (fun a e => f e a) l i}.forall (A : Type) (f : elt -> A -> A) (s : t) (i : A),
{r : A |
let (l, _) := elements s in
r = fold_left (fun (a : A) (e : elt) => f e a) l i}
  Proof.forall (A : Type) (f : elt -> A -> A) (s : t) (i : A),
{r : A |
let (l, _) := elements s in
r = fold_left (fun (a : A) (e : elt) => f e a) l i}
  intros; exists (fold (A:=A) f s i); exact (fold_1 s i f).
  Qed.

  Definition cardinal :
      forall s : t,
      {r : nat | let (l,_) := elements s in r = length l }.forall s : t,
{r : nat | let (l, _) := elements s in r = length l}
  Proof.forall s : t,
{r : nat | let (l, _) := elements s in r = length l}
    intros; exists (cardinal s); exact (cardinal_1 s).
  Qed.

  Definition fdec (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
    (x : elt) := if Pdec x then true else false.

  Lemma compat_P_aux :
   forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}),
   compat_P E.eq P -> compat_bool E.eq (fdec Pdec).forall (P : elt -> Prop)
  (Pdec : forall x : elt, {P x} + {~ P x}),
compat_P E.eq P -> compat_bool E.eq (fdec (P:=P) Pdec)
  Proof.forall (P : elt -> Prop)
  (Pdec : forall x : elt, {P x} + {~ P x}),
compat_P E.eq P -> compat_bool E.eq (fdec (P:=P) Pdec)
    unfold compat_P, compat_bool, Proper, respectful, fdec; intros.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {~ P x0}
H:forall x0 y0 : E.t,
E.eq x0 y0 -> impl (P x0) (P y0)
x, y:E.t
H0:E.eq x y
(if Pdec x then true else false) =
(if Pdec y then true else false)
    generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
  Qed.

  Hint Resolve compat_P_aux : core.

  Definition filter :
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t),
    {s' : t | compat_P E.eq P -> forall x : elt, In x s' <-> In x s /\ P x}.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{s' : t |
compat_P E.eq P ->
forall x : elt, In x s' <-> In x s /\ P x}
  Proof.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{s' : t |
compat_P E.eq P ->
forall x : elt, In x s' <-> In x s /\ P x}
    intros.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
{s' : t |
compat_P E.eq P ->
forall x : elt, In x s' <-> In x s /\ P x}
    exists (filter (fdec Pdec) s).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
compat_P E.eq P ->
forall x : elt,
In x (filter (fdec (P:=P) Pdec) s) <-> In x s /\ P x
    intro H; assert (compat_bool E.eq (fdec Pdec)); auto.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
forall x : elt,
In x (filter (fdec (P:=P) Pdec) s) <-> In x s /\ P x
    intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H1:In x (filter (fdec (P:=P) Pdec) s)
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H1:In x (filter (fdec (P:=P) Pdec) s)
P x
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
In x (filter (fdec (P:=P) Pdec) s)
    eauto with set.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H1:In x (filter (fdec (P:=P) Pdec) s)
P x
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
In x (filter (fdec (P:=P) Pdec) s)
    generalize (filter_2 H0 H1).P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H1:In x (filter (fdec (P:=P) Pdec) s)
fdec (P:=P) Pdec x = true -> P x
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
In x (filter (fdec (P:=P) Pdec) s)
    unfold fdec.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H1:In x (filter (fdec (P:=P) Pdec) s)
(if Pdec x then true else false) = true -> P x
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
In x (filter (fdec (P:=P) Pdec) s)
    case (Pdec x); intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H1:In x (filter (fdec (P:=P) Pdec) s)
f:P x -> False
H2:false = true
P x
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
In x (filter (fdec (P:=P) Pdec) s)
    inversion H2.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
In x (filter (fdec (P:=P) Pdec) s)
    apply filter_3; auto.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
fdec (P:=P) Pdec x = true
    unfold fdec; simpl.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_P E.eq P
H0:compat_bool E.eq (fdec (P:=P) Pdec)
x:elt
H2:In x s
H3:P x
(if Pdec x then true else false) = true
    case (Pdec x); intuition.
  Qed.

  Definition for_all :
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t),
    {compat_P E.eq P -> For_all P s} + {compat_P E.eq P -> ~ For_all P s}.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{compat_P E.eq P -> For_all P s} +
{compat_P E.eq P -> ~ For_all P s}
  Proof.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{compat_P E.eq P -> For_all P s} +
{compat_P E.eq P -> ~ For_all P s}
    intros.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
{compat_P E.eq P -> For_all P s} +
{compat_P E.eq P -> ~ For_all P s}
    generalize (for_all_1 (s:=s) (f:=fdec Pdec))
     (for_all_2 (s:=s) (f:=fdec Pdec)).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 For_all (fun x : elt => fdec (P:=P) Pdec x = true) s ->
 for_all (fdec (P:=P) Pdec) s = true) ->
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 for_all (fdec (P:=P) Pdec) s = true ->
 For_all (fun x : elt => fdec (P:=P) Pdec x = true) s) ->
{compat_P E.eq P -> For_all P s} +
{compat_P E.eq P -> ~ For_all P s}
    case (for_all (fdec Pdec) s); unfold For_all; [ left | right ];
     intros.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {~ P x0}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x0 : elt,
 In x0 s -> fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H2:In x s
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (forall x : elt, In x s -> P x)
    assert (compat_bool E.eq (fdec Pdec)); auto.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {~ P x0}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x0 : elt,
 In x0 s -> fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H2:In x s
H3:compat_bool E.eq (fdec (P:=P) Pdec)
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (forall x : elt, In x s -> P x)
    generalize (H0 H3 Logic.eq_refl _ H2).P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {~ P x0}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x0 : elt,
 In x0 s -> fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H2:In x s
H3:compat_bool E.eq (fdec (P:=P) Pdec)
fdec (P:=P) Pdec x = true -> P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (forall x : elt, In x s -> P x)
    unfold fdec.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {~ P x0}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x0 : elt,
 In x0 s -> fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H2:In x s
H3:compat_bool E.eq (fdec (P:=P) Pdec)
(if Pdec x then true else false) = true -> P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (forall x : elt, In x s -> P x)
    case (Pdec x); intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H1:compat_P E.eq P
x:elt
H2:In x s
H3:compat_bool E.eq (fdec (P:=P) Pdec)
n:P x -> False
H4:false = true
H0:forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H:true = true
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (forall x : elt, In x s -> P x)
    inversion H4.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (forall x : elt, In x s -> P x)
    intuition.P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
H2:forall x : elt, In x s -> P x
False
    absurd (false = true); [ auto with bool | apply H; auto ].P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x : elt,
 In x s -> fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x : elt,
In x s -> fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
H2:forall x : elt, In x s -> P x
forall x : elt, In x s -> fdec (P:=P) Pdec x = true
    intro.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x0 : elt,
 In x0 s -> fdec (P:=P) Pdec x0 = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
H2:forall x0 : elt, In x0 s -> P x0
x:elt
In x s -> fdec (P:=P) Pdec x = true
    unfold fdec.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(forall x0 : elt,
 In x0 s -> fdec (P:=P) Pdec x0 = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
forall x0 : elt,
In x0 s -> fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
H2:forall x0 : elt, In x0 s -> P x0
x:elt
In x s -> (if Pdec x then true else false) = true
    case (Pdec x); intuition.
  Qed.

  Definition exists_ :
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t),
    {compat_P E.eq P -> Exists P s} + {compat_P E.eq P -> ~ Exists P s}.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{compat_P E.eq P -> Exists P s} +
{compat_P E.eq P -> ~ Exists P s}
  Proof.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{compat_P E.eq P -> Exists P s} +
{compat_P E.eq P -> ~ Exists P s}
    intros.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
{compat_P E.eq P -> Exists P s} +
{compat_P E.eq P -> ~ Exists P s}
    generalize (exists_1 (s:=s) (f:=fdec Pdec))
     (exists_2 (s:=s) (f:=fdec Pdec)).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 Exists (fun x : elt => fdec (P:=P) Pdec x = true) s ->
 exists_ (fdec (P:=P) Pdec) s = true) ->
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 exists_ (fdec (P:=P) Pdec) s = true ->
 Exists (fun x : elt => fdec (P:=P) Pdec x = true) s) ->
{compat_P E.eq P -> Exists P s} +
{compat_P E.eq P -> ~ Exists P s}
    case (exists_ (fdec Pdec) s); unfold Exists; [ left | right ];
     intros.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
exists x : elt, In x s /\ P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    elim H0; auto; intros.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {~ P x0}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H2:In x s /\ fdec (P:=P) Pdec x = true
exists x0 : elt, In x0 s /\ P x0
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    exists x; intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H3:In x s
H4:fdec (P:=P) Pdec x = true
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    generalize H4.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H3:In x s
H4:fdec (P:=P) Pdec x = true
fdec (P:=P) Pdec x = true -> P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    unfold fdec.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H3:In x s
H4:fdec (P:=P) Pdec x = true
(if Pdec x then true else false) = true -> P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    case (Pdec x); intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
true = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
true = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
x:elt
H3:In x s
H4:fdec (P:=P) Pdec x = true
f:P x -> False
H2:false = true
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    inversion H2.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
~ (exists x : elt, In x s /\ P x)
    intuition.P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x : elt,
   In x s /\ fdec (P:=P) Pdec x = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x : elt,
  In x s /\ fdec (P:=P) Pdec x = true
H1:compat_P E.eq P
H2:exists x : elt, In x s /\ P x
False
    elim H2; intros.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
H2:exists x0 : elt, In x0 s /\ P x0
x:elt
H3:In x s /\ P x
False
    absurd (false = true); [ auto with bool | apply H; auto ].P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
H2:exists x0 : elt, In x0 s /\ P x0
x:elt
H3:In x s /\ P x
exists x0 : elt, In x0 s /\ fdec (P:=P) Pdec x0 = true
    exists x; intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
H2:exists x0 : elt, In x0 s /\ P x0
x:elt
H4:In x s
H5:P x
fdec (P:=P) Pdec x = true
    unfold fdec.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
(exists x0 : elt,
   In x0 s /\ fdec (P:=P) Pdec x0 = true) ->
false = true
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
false = true ->
exists x0 : elt,
  In x0 s /\ fdec (P:=P) Pdec x0 = true
H1:compat_P E.eq P
H2:exists x0 : elt, In x0 s /\ P x0
x:elt
H4:In x s
H5:P x
(if Pdec x then true else false) = true
    case (Pdec x); intuition.
  Qed.

  Definition partition :
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t),
    {partition : t * t |
    let (s1, s2) := partition in
    compat_P E.eq P ->
    For_all P s1 /\
    For_all (fun x => ~ P x) s2 /\
    (forall x : elt, In x s <-> In x s1 \/ In x s2)}.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{partition0 : t * t |
let (s1, s2) := partition0 in
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)}
  Proof.forall P : elt -> Prop,
(forall x : elt, {P x} + {~ P x}) ->
forall s : t,
{partition0 : t * t |
let (s1, s2) := partition0 in
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)}
    intros.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
{partition0 : t * t |
let (s1, s2) := partition0 in
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)}
    exists (partition (fdec Pdec) s).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
let (s1, s2) := partition (fdec (P:=P) Pdec) s in
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
    generalize (partition_1 s (f:=fdec Pdec)) (partition_2 s (f:=fdec Pdec)).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 fst (partition (fdec (P:=P) Pdec) s) [=]
 M.filter (fdec (P:=P) Pdec) s) ->
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 snd (partition (fdec (P:=P) Pdec) s) [=]
 M.filter (fun x : elt => negb (fdec (P:=P) Pdec x)) s) ->
let (s1, s2) := partition (fdec (P:=P) Pdec) s in
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
    case (partition (fdec Pdec) s).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s:t
forall t0 t1 : t,
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 fst (t0, t1) [=] M.filter (fdec (P:=P) Pdec) s) ->
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 snd (t0, t1) [=]
 M.filter (fun x : elt => negb (fdec (P:=P) Pdec x)) s) ->
compat_P E.eq P ->
For_all P t0 /\
For_all (fun x : elt => ~ P x) t1 /\
(forall x : elt, In x s <-> In x t0 \/ In x t1)
    intros s1 s2; simpl.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s, s1, s2:t
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 s1 [=] M.filter (fdec (P:=P) Pdec) s) ->
(compat_bool E.eq (fdec (P:=P) Pdec) ->
 s2 [=]
 M.filter (fun x : elt => negb (fdec (P:=P) Pdec x)) s) ->
compat_P E.eq P ->
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
    intros; assert (compat_bool E.eq (fdec Pdec)); auto.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s, s1, s2:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
s1 [=] M.filter (fdec (P:=P) Pdec) s
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
    intros; assert (compat_bool E.eq (fun x => negb (fdec Pdec x))).P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s, s1, s2:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
s1 [=] M.filter (fdec (P:=P) Pdec) s
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s, s1, s2:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
s1 [=] M.filter (fdec (P:=P) Pdec) s
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
    generalize H2; unfold compat_bool, Proper, respectful; intuition;
     apply (f_equal negb); auto.P:elt -> Prop
Pdec:forall x : elt, {P x} + {~ P x}
s, s1, s2:t
H:compat_bool E.eq (fdec (P:=P) Pdec) ->
s1 [=] M.filter (fdec (P:=P) Pdec) s
H0:compat_bool E.eq (fdec (P:=P) Pdec) ->
s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
For_all P s1 /\
For_all (fun x : elt => ~ P x) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
    intuition.P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all P s1
P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    generalize H4; unfold For_all, Equal; intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s1 <-> In a (M.filter (fdec (P:=P) Pdec) s)
x:elt
H5:In x s1
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    elim (H0 x); intros.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s1 <-> In a (M.filter (fdec (P:=P) Pdec) s)
x:elt
H5:In x s1
H6:In x s1 -> In x (M.filter (fdec (P:=P) Pdec) s)
H7:In x (M.filter (fdec (P:=P) Pdec) s) -> In x s1
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    assert (fdec Pdec x = true).P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s1 <-> In a (M.filter (fdec (P:=P) Pdec) s)
x:elt
H5:In x s1
H6:In x s1 -> In x (M.filter (fdec (P:=P) Pdec) s)
H7:In x (M.filter (fdec (P:=P) Pdec) s) -> In x s1
fdec (P:=P) Pdec x = true
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s1 <-> In a (M.filter (fdec (P:=P) Pdec) s)
x:elt
H5:In x s1
H6:In x s1 -> In x (M.filter (fdec (P:=P) Pdec) s)
H7:In x (M.filter (fdec (P:=P) Pdec) s) -> In x s1
H8:fdec (P:=P) Pdec x = true
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
     eapply filter_2; eauto with set.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s1 <-> In a (M.filter (fdec (P:=P) Pdec) s)
x:elt
H5:In x s1
H6:In x s1 -> In x (M.filter (fdec (P:=P) Pdec) s)
H7:In x (M.filter (fdec (P:=P) Pdec) s) -> In x s1
H8:fdec (P:=P) Pdec x = true
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    generalize H8; unfold fdec; case (Pdec x); intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s1 <-> In a (M.filter (fdec (P:=P) Pdec) s)
x:elt
H5:In x s1
H8:fdec (P:=P) Pdec x = true
f:P x -> False
H9:false = true
H10:In x (M.filter (fdec (P:=P) Pdec) s)
H6:In x s1
P x
P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    inversion H9.P:elt -> Prop
Pdec:forall x : elt, {P x} + {P x -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x : E.t => negb (fdec (P:=P) Pdec x))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x : elt => negb (fdec (P:=P) Pdec x)) s
For_all (fun x : elt => P x -> False) s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    generalize H; unfold For_all, Equal; intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s2 <->
In a
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
x:elt
H5:In x s2
H6:P x
False
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    elim (H0 x); intros.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s2 <->
In a
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
x:elt
H5:In x s2
H6:P x
H7:In x s2 ->
In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
H8:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
False
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    cut ((fun x => negb (fdec Pdec x)) x = true).P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s2 <->
In a
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
x:elt
H5:In x s2
H6:P x
H7:In x s2 ->
In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
H8:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
(fun x0 : elt => negb (fdec (P:=P) Pdec x0)) x = true ->
False
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s2 <->
In a
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
x:elt
H5:In x s2
H6:P x
H7:In x s2 ->
In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
H8:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
(fun x0 : elt => negb (fdec (P:=P) Pdec x0)) x = true
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    unfold fdec; case (Pdec x); intuition.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s2 <->
In a
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
x:elt
H5:In x s2
H6:P x
H7:In x s2 ->
In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
H8:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
(fun x0 : elt => negb (fdec (P:=P) Pdec x0)) x = true
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
      change ((fun x => negb (fdec Pdec x)) x = true).P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
H0:forall a : elt,
In a s2 <->
In a
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
x:elt
H5:In x s2
H6:P x
H7:In x s2 ->
In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s)
H8:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
(fun x0 : elt => negb (fdec (P:=P) Pdec x0)) x = true
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
      apply (filter_2 (s:=s) (x:=x)); auto.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
In x s1 \/ In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    set (b := fdec Pdec x) in *; generalize (Logic.eq_refl b);
     pattern b at -1; case b; unfold b;
     [ left | right ].P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
b:=fdec (P:=P) Pdec x:bool
H5:fdec (P:=P) Pdec x = true
In x s1
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
b:=fdec (P:=P) Pdec x:bool
H5:fdec (P:=P) Pdec x = false
In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    elim (H4 x); intros _ B; apply B; auto with set.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
b:=fdec (P:=P) Pdec x:bool
H5:fdec (P:=P) Pdec x = false
In x s2
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    elim (H x); intros _ B; apply B; auto with set.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
b:=fdec (P:=P) Pdec x:bool
H5:fdec (P:=P) Pdec x = false
B:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s)
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    apply filter_3; auto.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H0:In x s
b:=fdec (P:=P) Pdec x:bool
H5:fdec (P:=P) Pdec x = false
B:In x
  (M.filter
     (fun x0 : elt => negb (fdec (P:=P) Pdec x0))
     s) -> In x s2
negb (fdec (P:=P) Pdec x) = true
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    rewrite H5; auto.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s1
In x s
P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    eapply (filter_1 (s:=s) (x:=x) H2); elim (H4 x); intros B _; apply B;
     auto.P:elt -> Prop
Pdec:forall x0 : elt, {P x0} + {P x0 -> False}
s, s1, s2:t
H1:compat_P E.eq P
H2:compat_bool E.eq (fdec (P:=P) Pdec)
H3:compat_bool E.eq
  (fun x0 : E.t => negb (fdec (P:=P) Pdec x0))
H4:s1 [=] M.filter (fdec (P:=P) Pdec) s
H:s2 [=]
M.filter
  (fun x0 : elt => negb (fdec (P:=P) Pdec x0)) s
x:elt
H5:In x s2
In x s
    eapply (filter_1 (s:=s) (x:=x) H3); elim (H x); intros B _; apply B; auto.
  Qed.

  Definition choose_aux: forall s : t,
    { x : elt | M.choose s = Some x } + { M.choose s = None }.forall s : t,
{x : elt | choose s = Some x} + {choose s = None}
  Proof.forall s : t,
{x : elt | choose s = Some x} + {choose s = None}
   intros.s:t
{x : elt | choose s = Some x} + {choose s = None}
   destruct (M.choose s); [left | right]; auto.s:t
e:elt
{x : elt | Some e = Some x}
   exists e; auto.
  Qed.

  Definition choose : forall s : t, {x : elt | In x s} + {Empty s}.forall s : t, {x : elt | In x s} + {Empty s}
  Proof.forall s : t, {x : elt | In x s} + {Empty s}
   intros; destruct (choose_aux s) as [(x,Hx)|H].s:t
x:elt
Hx:choose s = Some x
{x0 : elt | In x0 s} + {Empty s}
s:t
H:choose s = None
{x : elt | In x s} + {Empty s}
   left; exists x; apply choose_1; auto.s:t
H:choose s = None
{x : elt | In x s} + {Empty s}
   right; apply choose_2; auto.
  Defined.

  Lemma choose_ok1 :
   forall s x, M.choose s = Some x <-> exists H:In x s,
      choose s = inleft _ (exist (fun x => In x s) x H).forall (s : t) (x : elt),
M.choose s = Some x <->
(exists H : In x s,
   choose s =
   inleft (exist (fun x0 : elt => In x0 s) x H))
  Proof.forall (s : t) (x : elt),
M.choose s = Some x <->
(exists H : In x s,
   choose s =
   inleft (exist (fun x0 : elt => In x0 s) x H))
    intros s x.s:t
x:elt
M.choose s = Some x <->
(exists H : In x s,
   choose s =
   inleft (exist (fun x0 : elt => In x0 s) x H))
    unfold choose; split; intros.s:t
x:elt
H:M.choose s = Some x
exists H0 : In x s,
  match choose_aux s with
  | inleft (exist _ x0 Hx) =>
      inleft
        (exist (fun x1 : elt => In x1 s) x0
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end = inleft (exist (fun x0 : elt => In x0 s) x H0)
s:t
x:elt
H:exists H0 : In x s,
  match choose_aux s with
  | inleft (exist _ x0 Hx) =>
      inleft
        (exist (fun x1 : elt => In x1 s) x0
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end =
  inleft (exist (fun x0 : elt => In x0 s) x H0)
M.choose s = Some x
    destruct (choose_aux s) as [(y,Hy)|H']; try congruence.s:t
x:elt
H:M.choose s = Some x
y:elt
Hy:M.choose s = Some y
exists H0 : In x s,
  inleft
    (exist (fun x0 : elt => In x0 s) y (choose_1 Hy)) =
  inleft (exist (fun x0 : elt => In x0 s) x H0)
s:t
x:elt
H:exists H0 : In x s,
  match choose_aux s with
  | inleft (exist _ x0 Hx) =>
      inleft
        (exist (fun x1 : elt => In x1 s) x0
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end =
  inleft (exist (fun x0 : elt => In x0 s) x H0)
M.choose s = Some x
    replace x with y in * by congruence.s:t
x, y:elt
H, Hy:M.choose s = Some y
exists H0 : In y s,
  inleft
    (exist (fun x0 : elt => In x0 s) y (choose_1 Hy)) =
  inleft (exist (fun x0 : elt => In x0 s) y H0)
s:t
x:elt
H:exists H0 : In x s,
  match choose_aux s with
  | inleft (exist _ x0 Hx) =>
      inleft
        (exist (fun x1 : elt => In x1 s) x0
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end =
  inleft (exist (fun x0 : elt => In x0 s) x H0)
M.choose s = Some x
    exists (choose_1 Hy); auto.s:t
x:elt
H:exists H0 : In x s,
  match choose_aux s with
  | inleft (exist _ x0 Hx) =>
      inleft
        (exist (fun x1 : elt => In x1 s) x0
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end =
  inleft (exist (fun x0 : elt => In x0 s) x H0)
M.choose s = Some x
    destruct H.s:t
x:elt
x0:In x s
H:match choose_aux s with
| inleft (exist _ x1 Hx) =>
    inleft
      (exist (fun x2 : elt => In x2 s) x1
         (choose_1 Hx))
| inright H0 => inright (choose_2 H0)
end =
inleft (exist (fun x1 : elt => In x1 s) x x0)
M.choose s = Some x
    destruct (choose_aux s) as [(y,Hy)|H']; congruence.
  Qed.

  Lemma choose_ok2 :
   forall s, M.choose s = None <-> exists H:Empty s,
      choose s = inright _ H.forall s : t,
M.choose s = None <->
(exists H : Empty s, choose s = inright H)
  Proof.forall s : t,
M.choose s = None <->
(exists H : Empty s, choose s = inright H)
    intros s.s:t
M.choose s = None <->
(exists H : Empty s, choose s = inright H)
    unfold choose; split; intros.s:t
H:M.choose s = None
exists H0 : Empty s,
  match choose_aux s with
  | inleft (exist _ x Hx) =>
      inleft
        (exist (fun x0 : elt => In x0 s) x
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end = inright H0
s:t
H:exists H0 : Empty s,
  match choose_aux s with
  | inleft (exist _ x Hx) =>
      inleft
        (exist (fun x0 : elt => In x0 s) x
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end = inright H0
M.choose s = None
    destruct (choose_aux s) as [(y,Hy)|H']; try congruence.s:t
H, H':M.choose s = None
exists H0 : Empty s,
  inright (choose_2 H') = inright H0
s:t
H:exists H0 : Empty s,
  match choose_aux s with
  | inleft (exist _ x Hx) =>
      inleft
        (exist (fun x0 : elt => In x0 s) x
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end = inright H0
M.choose s = None
    exists (choose_2 H'); auto.s:t
H:exists H0 : Empty s,
  match choose_aux s with
  | inleft (exist _ x Hx) =>
      inleft
        (exist (fun x0 : elt => In x0 s) x
           (choose_1 Hx))
  | inright H1 => inright (choose_2 H1)
  end = inright H0
M.choose s = None
    destruct H.s:t
x:Empty s
H:match choose_aux s with
| inleft (exist _ x0 Hx) =>
    inleft
      (exist (fun x1 : elt => In x1 s) x0
         (choose_1 Hx))
| inright H0 => inright (choose_2 H0)
end = inright x
M.choose s = None
    destruct (choose_aux s) as [(y,Hy)|H']; congruence.
  Qed.

  Lemma choose_equal : forall s s', Equal s s' ->
     match choose s, choose s' with
       | inleft (exist _ x _), inleft (exist _ x' _) => E.eq x x'
       | inright _, inright _  => True
       | _, _                        => False
     end.forall s s' : t,
s [=] s' ->
match choose s with
| inleft (exist _ x _) =>
    match choose s' with
    | inleft (exist _ x' _) => E.eq x x'
    | inright _ => False
    end
| inright _ => if choose s' then False else True
end
  Proof.forall s s' : t,
s [=] s' ->
match choose s with
| inleft (exist _ x _) =>
    match choose s' with
    | inleft (exist _ x' _) => E.eq x x'
    | inright _ => False
    end
| inright _ => if choose s' then False else True
end
   intros.s, s':t
H:s [=] s'
match choose s with
| inleft (exist _ x _) =>
    match choose s' with
    | inleft (exist _ x' _) => E.eq x x'
    | inright _ => False
    end
| inright _ => if choose s' then False else True
end
   generalize (@M.choose_1 s)(@M.choose_2 s)
              (@M.choose_1 s')(@M.choose_2 s')(@M.choose_3 s s')
              (choose_ok1 s)(choose_ok2 s)(choose_ok1 s')(choose_ok2 s').s, s':t
H:s [=] s'
(forall x : elt, M.choose s = Some x -> In x s) ->
(M.choose s = None -> Empty s) ->
(forall x : elt, M.choose s' = Some x -> In x s') ->
(M.choose s' = None -> Empty s') ->
(forall x y : elt,
 M.choose s = Some x ->
 M.choose s' = Some y -> s [=] s' -> E.eq x y) ->
(forall x : elt,
 M.choose s = Some x <->
 (exists H0 : In x s,
    choose s =
    inleft (exist (fun x0 : elt => In x0 s) x H0))) ->
M.choose s = None <->
(exists H0 : Empty s, choose s = inright H0) ->
(forall x : elt,
 M.choose s' = Some x <->
 (exists H0 : In x s',
    choose s' =
    inleft (exist (fun x0 : elt => In x0 s') x H0))) ->
M.choose s' = None <->
(exists H0 : Empty s', choose s' = inright H0) ->
match choose s with
| inleft (exist _ x _) =>
    match choose s' with
    | inleft (exist _ x' _) => E.eq x x'
    | inright _ => False
    end
| inright _ => if choose s' then False else True
end
   destruct (choose s) as [(x,Hx)|Hx]; destruct (choose s') as [(x',Hx')|Hx']; auto; intros.s, s':t
H:s [=] s'
x:elt
Hx:In x s
x':elt
Hx':In x' s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inleft
     (exist (fun x1 : elt => In x1 s') x' Hx') =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inright H9)
E.eq x x'
s, s':t
H:s [=] s'
x:elt
Hx:In x s
Hx':Empty s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inright Hx' =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s', inright Hx' = inright H9)
False
s, s':t
H:s [=] s'
Hx:Empty s
x':elt
Hx':In x' s'
H0:forall x : elt, M.choose s = Some x -> In x s
H1:M.choose s = None -> Empty s
H2:forall x : elt, M.choose s' = Some x -> In x s'
H3:M.choose s' = None -> Empty s'
H4:forall x y : elt,
M.choose s = Some x ->
M.choose s' = Some y -> s [=] s' -> E.eq x y
H5:forall x : elt,
M.choose s = Some x <->
(exists H9 : In x s,
   inright Hx =
   inleft (exist (fun x0 : elt => In x0 s) x H9))
H6:M.choose s = None <->
(exists H9 : Empty s, inright Hx = inright H9)
H7:forall x : elt,
M.choose s' = Some x <->
(exists H9 : In x s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inleft (exist (fun x0 : elt => In x0 s') x H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft (exist (fun x : elt => In x s') x' Hx') =
   inright H9)
False
   apply H4; auto.s, s':t
H:s [=] s'
x:elt
Hx:In x s
x':elt
Hx':In x' s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inleft
     (exist (fun x1 : elt => In x1 s') x' Hx') =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inright H9)
M.choose s = Some x
s, s':t
H:s [=] s'
x:elt
Hx:In x s
x':elt
Hx':In x' s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inleft
     (exist (fun x1 : elt => In x1 s') x' Hx') =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inright H9)
M.choose s' = Some x'
s, s':t
H:s [=] s'
x:elt
Hx:In x s
Hx':Empty s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inright Hx' =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s', inright Hx' = inright H9)
False
s, s':t
H:s [=] s'
Hx:Empty s
x':elt
Hx':In x' s'
H0:forall x : elt, M.choose s = Some x -> In x s
H1:M.choose s = None -> Empty s
H2:forall x : elt, M.choose s' = Some x -> In x s'
H3:M.choose s' = None -> Empty s'
H4:forall x y : elt,
M.choose s = Some x ->
M.choose s' = Some y -> s [=] s' -> E.eq x y
H5:forall x : elt,
M.choose s = Some x <->
(exists H9 : In x s,
   inright Hx =
   inleft (exist (fun x0 : elt => In x0 s) x H9))
H6:M.choose s = None <->
(exists H9 : Empty s, inright Hx = inright H9)
H7:forall x : elt,
M.choose s' = Some x <->
(exists H9 : In x s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inleft (exist (fun x0 : elt => In x0 s') x H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft (exist (fun x : elt => In x s') x' Hx') =
   inright H9)
False
   rewrite H5; exists Hx; auto.s, s':t
H:s [=] s'
x:elt
Hx:In x s
x':elt
Hx':In x' s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inleft
     (exist (fun x1 : elt => In x1 s') x' Hx') =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inright H9)
M.choose s' = Some x'
s, s':t
H:s [=] s'
x:elt
Hx:In x s
Hx':Empty s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inright Hx' =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s', inright Hx' = inright H9)
False
s, s':t
H:s [=] s'
Hx:Empty s
x':elt
Hx':In x' s'
H0:forall x : elt, M.choose s = Some x -> In x s
H1:M.choose s = None -> Empty s
H2:forall x : elt, M.choose s' = Some x -> In x s'
H3:M.choose s' = None -> Empty s'
H4:forall x y : elt,
M.choose s = Some x ->
M.choose s' = Some y -> s [=] s' -> E.eq x y
H5:forall x : elt,
M.choose s = Some x <->
(exists H9 : In x s,
   inright Hx =
   inleft (exist (fun x0 : elt => In x0 s) x H9))
H6:M.choose s = None <->
(exists H9 : Empty s, inright Hx = inright H9)
H7:forall x : elt,
M.choose s' = Some x <->
(exists H9 : In x s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inleft (exist (fun x0 : elt => In x0 s') x H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft (exist (fun x : elt => In x s') x' Hx') =
   inright H9)
False
   rewrite H7; exists Hx'; auto.s, s':t
H:s [=] s'
x:elt
Hx:In x s
Hx':Empty s'
H0:forall x0 : elt, M.choose s = Some x0 -> In x0 s
H1:M.choose s = None -> Empty s
H2:forall x0 : elt,
M.choose s' = Some x0 -> In x0 s'
H3:M.choose s' = None -> Empty s'
H4:forall x0 y : elt,
M.choose s = Some x0 ->
M.choose s' = Some y -> s [=] s' -> E.eq x0 y
H5:forall x0 : elt,
M.choose s = Some x0 <->
(exists H9 : In x0 s,
   inleft (exist (fun x1 : elt => In x1 s) x Hx) =
   inleft (exist (fun x1 : elt => In x1 s) x0 H9))
H6:M.choose s = None <->
(exists H9 : Empty s,
   inleft (exist (fun x0 : elt => In x0 s) x Hx) =
   inright H9)
H7:forall x0 : elt,
M.choose s' = Some x0 <->
(exists H9 : In x0 s',
   inright Hx' =
   inleft
     (exist (fun x1 : elt => In x1 s') x0 H9))
H8:M.choose s' = None <->
(exists H9 : Empty s', inright Hx' = inright H9)
False
s, s':t
H:s [=] s'
Hx:Empty s
x':elt
Hx':In x' s'
H0:forall x : elt, M.choose s = Some x -> In x s
H1:M.choose s = None -> Empty s
H2:forall x : elt, M.choose s' = Some x -> In x s'
H3:M.choose s' = None -> Empty s'
H4:forall x y : elt,
M.choose s = Some x ->
M.choose s' = Some y -> s [=] s' -> E.eq x y
H5:forall x : elt,
M.choose s = Some x <->
(exists H9 : In x s,
   inright Hx =
   inleft (exist (fun x0 : elt => In x0 s) x H9))
H6:M.choose s = None <->
(exists H9 : Empty s, inright Hx = inright H9)
H7:forall x : elt,
M.choose s' = Some x <->
(exists H9 : In x s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inleft (exist (fun x0 : elt => In x0 s') x H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft (exist (fun x : elt => In x s') x' Hx') =
   inright H9)
False
   apply Hx' with x; unfold Equal in H; rewrite <-H; auto.s, s':t
H:s [=] s'
Hx:Empty s
x':elt
Hx':In x' s'
H0:forall x : elt, M.choose s = Some x -> In x s
H1:M.choose s = None -> Empty s
H2:forall x : elt, M.choose s' = Some x -> In x s'
H3:M.choose s' = None -> Empty s'
H4:forall x y : elt,
M.choose s = Some x ->
M.choose s' = Some y -> s [=] s' -> E.eq x y
H5:forall x : elt,
M.choose s = Some x <->
(exists H9 : In x s,
   inright Hx =
   inleft (exist (fun x0 : elt => In x0 s) x H9))
H6:M.choose s = None <->
(exists H9 : Empty s, inright Hx = inright H9)
H7:forall x : elt,
M.choose s' = Some x <->
(exists H9 : In x s',
   inleft
     (exist (fun x0 : elt => In x0 s') x' Hx') =
   inleft (exist (fun x0 : elt => In x0 s') x H9))
H8:M.choose s' = None <->
(exists H9 : Empty s',
   inleft (exist (fun x : elt => In x s') x' Hx') =
   inright H9)
False
   apply Hx with x'; unfold Equal in H; rewrite H; auto.
  Qed.

  Definition min_elt :
    forall s : t,
    {x : elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}.forall s : t,
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt y x) s} +
{Empty s}
  Proof.forall s : t,
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt y x) s} +
{Empty s}
    intros;
     generalize (min_elt_1 (s:=s)) (min_elt_2 (s:=s)) (min_elt_3 (s:=s)).s:t
(forall x : elt, min_elt s = Some x -> In x s) ->
(forall x y : elt,
 min_elt s = Some x -> In y s -> ~ E.lt y x) ->
(min_elt s = None -> Empty s) ->
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt y x) s} +
{Empty s}
    case (min_elt s); [ left | right ]; auto.s:t
e:elt
H:forall x : elt, Some e = Some x -> In x s
H0:forall x y : elt,
Some e = Some x -> In y s -> ~ E.lt y x
H1:Some e = None -> Empty s
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt y x) s}
    exists e; unfold For_all; eauto.
  Qed.

  Definition max_elt :
    forall s : t,
    {x : elt | In x s /\ For_all (fun y => ~ E.lt x y) s} + {Empty s}.forall s : t,
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt x y) s} +
{Empty s}
  Proof.forall s : t,
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt x y) s} +
{Empty s}
    intros;
     generalize (max_elt_1 (s:=s)) (max_elt_2 (s:=s)) (max_elt_3 (s:=s)).s:t
(forall x : elt, max_elt s = Some x -> In x s) ->
(forall x y : elt,
 max_elt s = Some x -> In y s -> ~ E.lt x y) ->
(max_elt s = None -> Empty s) ->
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt x y) s} +
{Empty s}
    case (max_elt s); [ left | right ]; auto.s:t
e:elt
H:forall x : elt, Some e = Some x -> In x s
H0:forall x y : elt,
Some e = Some x -> In y s -> ~ E.lt x y
H1:Some e = None -> Empty s
{x : elt |
In x s /\ For_all (fun y : elt => ~ E.lt x y) s}
    exists e; unfold For_all; eauto.
  Qed.

  Definition elt := elt.
  Definition t := t.

  Definition In := In.
  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
  Definition Subset s s' := forall a : elt, In a s -> In a s'.
  Definition Empty s := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) (s : t) :=
    forall x : elt, In x s -> P x.
  Definition Exists (P : elt -> Prop) (s : t) :=
    exists x : elt, In x s /\ P x.

  Definition eq_In := In_1.

  Definition eq := Equal.
  Definition lt := lt.
  Definition eq_refl := eq_refl.
  Definition eq_sym := eq_sym.
  Definition eq_trans := eq_trans.
  Definition lt_trans := lt_trans.
  Definition lt_not_eq := lt_not_eq.
  Definition compare := compare.

  Module E := E.

End DepOfNodep.

From dependent signature Sdep to non-dependent signature S.

Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
  Import M.

  Module ME := OrderedTypeFacts E.

  Definition empty : t := let (s, _) := empty in s.

  Lemma empty_1 : Empty empty.Empty empty
  Proof.Empty empty
    unfold empty; case M.empty; auto.
  Qed.

  Definition is_empty (s : t) : bool :=
    if is_empty s then true else false.

  Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.forall s : t, Empty s -> is_empty s = true
  Proof.forall s : t, Empty s -> is_empty s = true
    intros; unfold is_empty; case (M.is_empty s); auto.
  Qed.

  Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.forall s : t, is_empty s = true -> Empty s
  Proof.forall s : t, is_empty s = true -> Empty s
    intro s; unfold is_empty; case (M.is_empty s); auto.s:t
~ Empty s -> false = true -> Empty s
    intros; discriminate H.
  Qed.

  Definition mem (x : elt) (s : t) : bool :=
    if mem x s then true else false.

  Lemma mem_1 : forall (s : t) (x : elt), In x s -> mem x s = true.forall (s : t) (x : elt), In x s -> mem x s = true
  Proof.forall (s : t) (x : elt), In x s -> mem x s = true
    intros; unfold mem; case (M.mem x s); auto.
  Qed.

  Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.forall (s : t) (x : elt), mem x s = true -> In x s
  Proof.forall (s : t) (x : elt), mem x s = true -> In x s
    intros s x; unfold mem; case (M.mem x s); auto.s:t
x:elt
~ In x s -> false = true -> In x s
    intros; discriminate H.
  Qed.

  Definition eq_dec := equal.

  Definition equal (s s' : t) : bool :=
    if equal s s' then true else false.

  Lemma equal_1 : forall s s' : t, Equal s s' -> equal s s' = true.forall s s' : t, s [=] s' -> equal s s' = true
  Proof.forall s s' : t, s [=] s' -> equal s s' = true
    intros; unfold equal; case M.equal; intuition.
  Qed.

  Lemma equal_2 : forall s s' : t, equal s s' = true -> Equal s s'.forall s s' : t, equal s s' = true -> s [=] s'
  Proof.forall s s' : t, equal s s' = true -> s [=] s'
    intros s s'; unfold equal; case (M.equal s s'); intuition;
     inversion H.
  Qed.

  Definition subset (s s' : t) : bool :=
    if subset s s' then true else false.

  Lemma subset_1 : forall s s' : t, Subset s s' -> subset s s' = true.forall s s' : t, Subset s s' -> subset s s' = true
  Proof.forall s s' : t, Subset s s' -> subset s s' = true
    intros; unfold subset; case M.subset; intuition.
  Qed.

  Lemma subset_2 : forall s s' : t, subset s s' = true -> Subset s s'.forall s s' : t, subset s s' = true -> Subset s s'
  Proof.forall s s' : t, subset s s' = true -> Subset s s'
    intros s s'; unfold subset; case (M.subset s s'); intuition;
     inversion H.
  Qed.

  Definition choose (s : t) : option elt :=
    match choose s with
    | inleft (exist _ x _) => Some x
    | inright _ => None
    end.

  Lemma choose_1 : forall (s : t) (x : elt), choose s = Some x -> In x s.forall (s : t) (x : elt), choose s = Some x -> In x s
  Proof.forall (s : t) (x : elt), choose s = Some x -> In x s
    intros s x; unfold choose; case (M.choose s).s:t
x:elt
forall s0 : {x0 : elt | In x0 s},
(let (x0, _) := s0 in Some x0) = Some x -> In x s
s:t
x:elt
Empty s -> None = Some x -> In x s
    simple destruct s0; intros; injection H; intros; subst; auto.s:t
x:elt
Empty s -> None = Some x -> In x s
    intros; discriminate H.
  Qed.

  Lemma choose_2 : forall s : t, choose s = None -> Empty s.forall s : t, choose s = None -> Empty s
  Proof.forall s : t, choose s = None -> Empty s
    intro s; unfold choose; case (M.choose s); auto.s:t
forall s0 : {x : elt | In x s},
(let (x, _) := s0 in Some x) = None -> Empty s
    simple destruct s0; intros; discriminate H.
  Qed.

  Lemma choose_3 : forall s s' x x',
   choose s = Some x -> choose s' = Some x' -> Equal s s' -> E.eq x x'.forall (s s' : t) (x x' : elt),
choose s = Some x ->
choose s' = Some x' -> s [=] s' -> E.eq x x'
  Proof.forall (s s' : t) (x x' : elt),
choose s = Some x ->
choose s' = Some x' -> s [=] s' -> E.eq x x'
  unfold choose; intros.s, s':t
x, x':elt
H:match M.choose s with
| inleft (exist _ x0 _) => Some x0
| inright _ => None
end = Some x
H0:match M.choose s' with
| inleft (exist _ x0 _) => Some x0
| inright _ => None
end = Some x'
H1:s [=] s'
E.eq x x'
  generalize (M.choose_equal H1); clear H1.s, s':t
x, x':elt
H:match M.choose s with
| inleft (exist _ x0 _) => Some x0
| inright _ => None
end = Some x
H0:match M.choose s' with
| inleft (exist _ x0 _) => Some x0
| inright _ => None
end = Some x'
match M.choose s with
| inleft (exist _ x0 _) =>
    match M.choose s' with
    | inleft (exist _ x'0 _) => E.eq x0 x'0
    | inright _ => False
    end
| inright _ => if M.choose s' then False else True
end -> E.eq x x'
  destruct (M.choose s) as [(?,?)|?]; destruct (M.choose s') as [(?,?)|?];
   simpl; auto; congruence.
  Qed.

  Definition elements (s : t) : list elt := let (l, _) := elements s in l.

  Lemma elements_1 : forall (s : t) (x : elt), In x s -> InA E.eq x (elements s).forall (s : t) (x : elt),
In x s -> InA E.eq x (elements s)
  Proof.forall (s : t) (x : elt),
In x s -> InA E.eq x (elements s)
    intros; unfold elements; case (M.elements s); firstorder.
  Qed.

  Lemma elements_2 : forall (s : t) (x : elt), InA E.eq x (elements s) -> In x s.forall (s : t) (x : elt),
InA E.eq x (elements s) -> In x s
  Proof.forall (s : t) (x : elt),
InA E.eq x (elements s) -> In x s
    intros s x; unfold elements; case (M.elements s); firstorder.
  Qed.

  Lemma elements_3 : forall s : t, sort E.lt (elements s).forall s : t, Sorted E.lt (elements s)
  Proof.forall s : t, Sorted E.lt (elements s)
    intros; unfold elements; case (M.elements s); firstorder.
  Qed.
  Hint Resolve elements_3 : core.

  Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).forall s : t, NoDupA E.eq (elements s)
  Proof.forall s : t, NoDupA E.eq (elements s) auto. Qed.

  Definition min_elt (s : t) : option elt :=
    match min_elt s with
    | inleft (exist _ x _) => Some x
    | inright _ => None
    end.

  Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.forall (s : t) (x : elt), min_elt s = Some x -> In x s
  Proof.forall (s : t) (x : elt), min_elt s = Some x -> In x s
    intros s x; unfold min_elt; case (M.min_elt s).s:t
x:elt
forall
  s0 : {x0 : elt |
       In x0 s /\
       For_all (fun y : elt => ~ E.lt y x0) s},
(let (x0, _) := s0 in Some x0) = Some x -> In x s
s:t
x:elt
Empty s -> None = Some x -> In x s
    simple destruct s0; intros; injection H; intros; subst; intuition.s:t
x:elt
Empty s -> None = Some x -> In x s
    intros; discriminate H.
  Qed.

  Lemma min_elt_2 :
   forall (s : t) (x y : elt), min_elt s = Some x -> In y s -> ~ E.lt y x.forall (s : t) (x y : elt),
min_elt s = Some x -> In y s -> ~ E.lt y x
  Proof.forall (s : t) (x y : elt),
min_elt s = Some x -> In y s -> ~ E.lt y x
    intros s x y; unfold min_elt; case (M.min_elt s).s:t
x, y:elt
forall
  s0 : {x0 : elt |
       In x0 s /\
       For_all (fun y0 : elt => ~ E.lt y0 x0) s},
(let (x0, _) := s0 in Some x0) = Some x ->
In y s -> ~ E.lt y x
s:t
x, y:elt
Empty s -> None = Some x -> In y s -> ~ E.lt y x
    unfold For_all; simple destruct s0; intros; injection H; intros;
     subst; firstorder.s:t
x, y:elt
Empty s -> None = Some x -> In y s -> ~ E.lt y x
    intros; discriminate H.
  Qed.

  Lemma min_elt_3 : forall s : t, min_elt s = None -> Empty s.forall s : t, min_elt s = None -> Empty s
  Proof.forall s : t, min_elt s = None -> Empty s
    intros s; unfold min_elt; case (M.min_elt s); auto.s:t
forall
  s0 : {x : elt |
       In x s /\ For_all (fun y : elt => ~ E.lt y x) s},
(let (x, _) := s0 in Some x) = None -> Empty s
    simple destruct s0; intros; discriminate H.
  Qed.

  Definition max_elt (s : t) : option elt :=
    match max_elt s with
    | inleft (exist _ x _) => Some x
    | inright _ => None
    end.

  Lemma max_elt_1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.forall (s : t) (x : elt), max_elt s = Some x -> In x s
  Proof.forall (s : t) (x : elt), max_elt s = Some x -> In x s
    intros s x; unfold max_elt; case (M.max_elt s).s:t
x:elt
forall
  s0 : {x0 : elt |
       In x0 s /\
       For_all (fun y : elt => ~ E.lt x0 y) s},
(let (x0, _) := s0 in Some x0) = Some x -> In x s
s:t
x:elt
Empty s -> None = Some x -> In x s
    simple destruct s0; intros; injection H; intros; subst; intuition.s:t
x:elt
Empty s -> None = Some x -> In x s
    intros; discriminate H.
  Qed.

  Lemma max_elt_2 :
   forall (s : t) (x y : elt), max_elt s = Some x -> In y s -> ~ E.lt x y.forall (s : t) (x y : elt),
max_elt s = Some x -> In y s -> ~ E.lt x y
  Proof.forall (s : t) (x y : elt),
max_elt s = Some x -> In y s -> ~ E.lt x y
    intros s x y; unfold max_elt; case (M.max_elt s).s:t
x, y:elt
forall
  s0 : {x0 : elt |
       In x0 s /\
       For_all (fun y0 : elt => ~ E.lt x0 y0) s},
(let (x0, _) := s0 in Some x0) = Some x ->
In y s -> ~ E.lt x y
s:t
x, y:elt
Empty s -> None = Some x -> In y s -> ~ E.lt x y
    unfold For_all; simple destruct s0; intros; injection H; intros;
     subst; firstorder.s:t
x, y:elt
Empty s -> None = Some x -> In y s -> ~ E.lt x y
    intros; discriminate H.
  Qed.

  Lemma max_elt_3 : forall s : t, max_elt s = None -> Empty s.forall s : t, max_elt s = None -> Empty s
  Proof.forall s : t, max_elt s = None -> Empty s
    intros s; unfold max_elt; case (M.max_elt s); auto.s:t
forall
  s0 : {x : elt |
       In x s /\ For_all (fun y : elt => ~ E.lt x y) s},
(let (x, _) := s0 in Some x) = None -> Empty s
    simple destruct s0; intros; discriminate H.
  Qed.

  Definition add (x : elt) (s : t) : t := let (s', _) := add x s in s'.

  Lemma add_1 : forall (s : t) (x y : elt), E.eq x y -> In y (add x s).forall (s : t) (x y : elt), E.eq x y -> In y (add x s)
  Proof.forall (s : t) (x y : elt), E.eq x y -> In y (add x s)
    intros; unfold add; case (M.add x s); unfold Add;
     firstorder.
  Qed.

  Lemma add_2 : forall (s : t) (x y : elt), In y s -> In y (add x s).forall (s : t) (x y : elt), In y s -> In y (add x s)
  Proof.forall (s : t) (x y : elt), In y s -> In y (add x s)
    intros; unfold add; case (M.add x s); unfold Add;
     firstorder.
  Qed.

  Lemma add_3 :
   forall (s : t) (x y : elt), ~ E.eq x y -> In y (add x s) -> In y s.forall (s : t) (x y : elt),
~ E.eq x y -> In y (add x s) -> In y s
  Proof.forall (s : t) (x y : elt),
~ E.eq x y -> In y (add x s) -> In y s
    intros s x y; unfold add; case (M.add x s); unfold Add;
     firstorder.
  Qed.

  Definition remove (x : elt) (s : t) : t := let (s', _) := remove x s in s'.

  Lemma remove_1 : forall (s : t) (x y : elt), E.eq x y -> ~ In y (remove x s).forall (s : t) (x y : elt),
E.eq x y -> ~ In y (remove x s)
  Proof.forall (s : t) (x y : elt),
E.eq x y -> ~ In y (remove x s)
    intros; unfold remove; case (M.remove x s); firstorder.
  Qed.

  Lemma remove_2 :
   forall (s : t) (x y : elt), ~ E.eq x y -> In y s -> In y (remove x s).forall (s : t) (x y : elt),
~ E.eq x y -> In y s -> In y (remove x s)
  Proof.forall (s : t) (x y : elt),
~ E.eq x y -> In y s -> In y (remove x s)
    intros; unfold remove; case (M.remove x s); firstorder.
  Qed.

  Lemma remove_3 : forall (s : t) (x y : elt), In y (remove x s) -> In y s.forall (s : t) (x y : elt),
In y (remove x s) -> In y s
  Proof.forall (s : t) (x y : elt),
In y (remove x s) -> In y s
    intros s x y; unfold remove; case (M.remove x s); firstorder.
  Qed.

  Definition singleton (x : elt) : t := let (s, _) := singleton x in s.

  Lemma singleton_1 : forall x y : elt, In y (singleton x) -> E.eq x y.forall x y : elt, In y (singleton x) -> E.eq x y
  Proof.forall x y : elt, In y (singleton x) -> E.eq x y
    intros x y; unfold singleton; case (M.singleton x); firstorder.
  Qed.

  Lemma singleton_2 : forall x y : elt, E.eq x y -> In y (singleton x).forall x y : elt, E.eq x y -> In y (singleton x)
  Proof.forall x y : elt, E.eq x y -> In y (singleton x)
    intros x y; unfold singleton; case (M.singleton x); firstorder.
  Qed.

  Definition union (s s' : t) : t := let (s'', _) := union s s' in s''.

  Lemma union_1 :
   forall (s s' : t) (x : elt), In x (union s s') -> In x s \/ In x s'.forall (s s' : t) (x : elt),
In x (union s s') -> In x s \/ In x s'
  Proof.forall (s s' : t) (x : elt),
In x (union s s') -> In x s \/ In x s'
    intros s s' x; unfold union; case (M.union s s'); firstorder.
  Qed.

  Lemma union_2 : forall (s s' : t) (x : elt), In x s -> In x (union s s').forall (s s' : t) (x : elt),
In x s -> In x (union s s')
  Proof.forall (s s' : t) (x : elt),
In x s -> In x (union s s')
    intros s s' x; unfold union; case (M.union s s'); firstorder.
  Qed.

  Lemma union_3 : forall (s s' : t) (x : elt), In x s' -> In x (union s s').forall (s s' : t) (x : elt),
In x s' -> In x (union s s')
  Proof.forall (s s' : t) (x : elt),
In x s' -> In x (union s s')
    intros s s' x; unfold union; case (M.union s s'); firstorder.
  Qed.

  Definition inter (s s' : t) : t := let (s'', _) := inter s s' in s''.

  Lemma inter_1 : forall (s s' : t) (x : elt), In x (inter s s') -> In x s.forall (s s' : t) (x : elt),
In x (inter s s') -> In x s
  Proof.forall (s s' : t) (x : elt),
In x (inter s s') -> In x s
    intros s s' x; unfold inter; case (M.inter s s'); firstorder.
  Qed.

  Lemma inter_2 : forall (s s' : t) (x : elt), In x (inter s s') -> In x s'.forall (s s' : t) (x : elt),
In x (inter s s') -> In x s'
  Proof.forall (s s' : t) (x : elt),
In x (inter s s') -> In x s'
    intros s s' x; unfold inter; case (M.inter s s'); firstorder.
  Qed.

  Lemma inter_3 :
   forall (s s' : t) (x : elt), In x s -> In x s' -> In x (inter s s').forall (s s' : t) (x : elt),
In x s -> In x s' -> In x (inter s s')
  Proof.forall (s s' : t) (x : elt),
In x s -> In x s' -> In x (inter s s')
    intros s s' x; unfold inter; case (M.inter s s'); firstorder.
  Qed.

  Definition diff (s s' : t) : t := let (s'', _) := diff s s' in s''.

  Lemma diff_1 : forall (s s' : t) (x : elt), In x (diff s s') -> In x s.forall (s s' : t) (x : elt),
In x (diff s s') -> In x s
  Proof.forall (s s' : t) (x : elt),
In x (diff s s') -> In x s
    intros s s' x; unfold diff; case (M.diff s s'); firstorder.
  Qed.

  Lemma diff_2 : forall (s s' : t) (x : elt), In x (diff s s') -> ~ In x s'.forall (s s' : t) (x : elt),
In x (diff s s') -> ~ In x s'
  Proof.forall (s s' : t) (x : elt),
In x (diff s s') -> ~ In x s'
    intros s s' x; unfold diff; case (M.diff s s'); firstorder.
  Qed.

  Lemma diff_3 :
   forall (s s' : t) (x : elt), In x s -> ~ In x s' -> In x (diff s s').forall (s s' : t) (x : elt),
In x s -> ~ In x s' -> In x (diff s s')
  Proof.forall (s s' : t) (x : elt),
In x s -> ~ In x s' -> In x (diff s s')
    intros s s' x; unfold diff; case (M.diff s s'); firstorder.
  Qed.

  Definition cardinal (s : t) : nat := let (f, _) := cardinal s in f.

  Lemma cardinal_1 : forall s, cardinal s = length (elements s).forall s : t, cardinal s = length (elements s)
  Proof.forall s : t, cardinal s = length (elements s)
    intros; unfold cardinal; case (M.cardinal s); unfold elements in *;
    destruct (M.elements s); auto.
  Qed.

  Definition fold (B : Type) (f : elt -> B -> B) (i : t)
    (s : B) : B := let (fold, _) := fold f i s in fold.

  Lemma fold_1 :
   forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
   fold f s i = fold_left (fun a e => f e a) (elements s) i.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i =
fold_left (fun (a : A) (e : elt) => f e a)
  (elements s) i
  Proof.forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
fold f s i =
fold_left (fun (a : A) (e : elt) => f e a)
  (elements s) i
    intros; unfold fold; case (M.fold f s i); unfold elements in *;
    destruct (M.elements s); auto.
  Qed.

  Definition f_dec :
    forall (f : elt -> bool) (x : elt), {f x = true} + {f x <> true}.forall (f : elt -> bool) (x : elt),
{f x = true} + {f x <> true}
  Proof.forall (f : elt -> bool) (x : elt),
{f x = true} + {f x <> true}
    intros; case (f x); auto with bool.
  Defined.

  Lemma compat_P_aux :
   forall f : elt -> bool,
   compat_bool E.eq f -> compat_P E.eq (fun x => f x = true).forall f : elt -> bool,
compat_bool E.eq f ->
compat_P E.eq (fun x : E.t => f x = true)
  Proof.forall f : elt -> bool,
compat_bool E.eq f ->
compat_P E.eq (fun x : E.t => f x = true)
     unfold compat_bool, compat_P, Proper, respectful, impl; intros;
      rewrite <- H1; firstorder.
  Qed.

  Hint Resolve compat_P_aux : core.

  Definition filter (f : elt -> bool) (s : t) : t :=
    let (s', _) := filter (P:=fun x => f x = true) (f_dec f) s in s'.

  Lemma filter_1 :
   forall (s : t) (x : elt) (f : elt -> bool),
   compat_bool E.eq f -> In x (filter f s) -> In x s.forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x (filter f s) -> In x s
  Proof.forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x (filter f s) -> In x s
    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.s:t
x:elt
f:elt -> bool
x0:t
Hiff:compat_P E.eq (fun x1 : elt => f x1 = true) ->
forall x1 : elt,
In x1 x0 <-> In x1 s /\ f x1 = true
H:compat_bool E.eq f
H0:In x x0
In x s
    generalize (Hiff (compat_P_aux H)); firstorder.
  Qed.

  Lemma filter_2 :
   forall (s : t) (x : elt) (f : elt -> bool),
   compat_bool E.eq f -> In x (filter f s) -> f x = true.forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x (filter f s) -> f x = true
  Proof.forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f -> In x (filter f s) -> f x = true
    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.s:t
x:elt
f:elt -> bool
x0:t
Hiff:compat_P E.eq (fun x1 : elt => f x1 = true) ->
forall x1 : elt,
In x1 x0 <-> In x1 s /\ f x1 = true
H:compat_bool E.eq f
H0:In x x0
f x = true
    generalize (Hiff (compat_P_aux H)); firstorder.
  Qed.

  Lemma filter_3 :
   forall (s : t) (x : elt) (f : elt -> bool),
   compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f ->
In x s -> f x = true -> In x (filter f s)
  Proof.forall (s : t) (x : elt) (f : elt -> bool),
compat_bool E.eq f ->
In x s -> f x = true -> In x (filter f s)
    intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition.s:t
x:elt
f:elt -> bool
x0:t
Hiff:compat_P E.eq (fun x1 : elt => f x1 = true) ->
forall x1 : elt,
In x1 x0 <-> In x1 s /\ f x1 = true
H:compat_bool E.eq f
H0:In x s
H1:f x = true
In x x0
    generalize (Hiff (compat_P_aux H)); firstorder.
  Qed.

  Definition for_all (f : elt -> bool) (s : t) : bool :=
    if for_all (P:=fun x => f x = true) (f_dec f) s
    then true
    else false.

  Lemma for_all_1 :
   forall (s : t) (f : elt -> bool),
   compat_bool E.eq f ->
   For_all (fun x => f x = true) s -> for_all f s = true.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
For_all (fun x : elt => f x = true) s ->
for_all f s = true
  Proof.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
For_all (fun x : elt => f x = true) s ->
for_all f s = true
    intros s f; unfold for_all; case M.for_all; intuition; elim n;
     auto.
  Qed.

  Lemma for_all_2 :
   forall (s : t) (f : elt -> bool),
   compat_bool E.eq f ->
   for_all f s = true -> For_all (fun x => f x = true) s.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
for_all f s = true ->
For_all (fun x : elt => f x = true) s
  Proof.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
for_all f s = true ->
For_all (fun x : elt => f x = true) s
    intros s f; unfold for_all; case M.for_all; intuition;
     inversion H0.
  Qed.

  Definition exists_ (f : elt -> bool) (s : t) : bool :=
    if exists_ (P:=fun x => f x = true) (f_dec f) s
    then true
    else false.

  Lemma exists_1 :
   forall (s : t) (f : elt -> bool),
   compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
Exists (fun x : elt => f x = true) s ->
exists_ f s = true
  Proof.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
Exists (fun x : elt => f x = true) s ->
exists_ f s = true
    intros s f; unfold exists_; case M.exists_; intuition; elim n;
     auto.
  Qed.

  Lemma exists_2 :
   forall (s : t) (f : elt -> bool),
   compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
exists_ f s = true ->
Exists (fun x : elt => f x = true) s
  Proof.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
exists_ f s = true ->
Exists (fun x : elt => f x = true) s
    intros s f; unfold exists_; case M.exists_; intuition;
     inversion H0.
  Qed.

  Definition partition (f : elt -> bool) (s : t) :
    t * t :=
    let (p, _) := partition (P:=fun x => f x = true) (f_dec f) s in p.

  Lemma partition_1 :
   forall (s : t) (f : elt -> bool),
   compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
fst (partition f s) [=] filter f s
  Proof.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
fst (partition f s) [=] filter f s
    intros s f; unfold partition; case M.partition.s:t
f:elt -> bool
forall x : t * t,
(let (s1, s2) := x in
 compat_P E.eq (fun x0 : elt => f x0 = true) ->
 For_all (fun x0 : elt => f x0 = true) s1 /\
 For_all (fun x0 : elt => f x0 <> true) s2 /\
 (forall x0 : elt, In x0 s <-> In x0 s1 \/ In x0 s2)) ->
compat_bool E.eq f -> fst x [=] filter f s
    intro p; case p; clear p; intros s1 s2 H C.s:t
f:elt -> bool
s1, s2:t
H:compat_P E.eq (fun x : elt => f x = true) ->
For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
C:compat_bool E.eq f
fst (s1, s2) [=] filter f s
    generalize (H (compat_P_aux C)); clear H; intro H.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H:For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
fst (s1, s2) [=] filter f s
    simpl; unfold Equal; intuition.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a s1
In a (filter f s)
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
In a s1
    apply filter_3; firstorder.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
In a s1
    elim (H2 a); intros.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
In a s1
    assert (In a s).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
In a s
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
In a s1
     eapply filter_1; eauto.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
In a s1
    elim H3; intros; auto.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s2
In a s1
    absurd (f a = true).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s2
f a <> true
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s2
f a = true
    exact (H a H6).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter f s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s2
f a = true
    eapply filter_2; eauto.
  Qed.

  Lemma partition_2 :
   forall (s : t) (f : elt -> bool),
   compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
snd (partition f s)
[=] filter (fun x : elt => negb (f x)) s
  Proof.forall (s : t) (f : elt -> bool),
compat_bool E.eq f ->
snd (partition f s)
[=] filter (fun x : elt => negb (f x)) s
    intros s f; unfold partition; case M.partition.s:t
f:elt -> bool
forall x : t * t,
(let (s1, s2) := x in
 compat_P E.eq (fun x0 : elt => f x0 = true) ->
 For_all (fun x0 : elt => f x0 = true) s1 /\
 For_all (fun x0 : elt => f x0 <> true) s2 /\
 (forall x0 : elt, In x0 s <-> In x0 s1 \/ In x0 s2)) ->
compat_bool E.eq f ->
snd x [=] filter (fun x0 : elt => negb (f x0)) s
    intro p; case p; clear p; intros s1 s2 H C.s:t
f:elt -> bool
s1, s2:t
H:compat_P E.eq (fun x : elt => f x = true) ->
For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
C:compat_bool E.eq f
snd (s1, s2) [=] filter (fun x : elt => negb (f x)) s
    generalize (H (compat_P_aux C)); clear H; intro H.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H:For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
snd (s1, s2) [=] filter (fun x : elt => negb (f x)) s
    assert (D : compat_bool E.eq (fun x => negb (f x))).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H:For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
compat_bool E.eq (fun x : E.t => negb (f x))
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H:For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
D:compat_bool E.eq (fun x : E.t => negb (f x))
snd (s1, s2) [=] filter (fun x : elt => negb (f x)) s
    generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
     auto.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
H:For_all (fun x : elt => f x = true) s1 /\
For_all (fun x : elt => f x <> true) s2 /\
(forall x : elt, In x s <-> In x s1 \/ In x s2)
D:compat_bool E.eq (fun x : E.t => negb (f x))
snd (s1, s2) [=] filter (fun x : elt => negb (f x)) s
    simpl; unfold Equal; intuition.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a s2
In a (filter (fun x : elt => negb (f x)) s)
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
In a s2
    apply filter_3; firstorder.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
In a s2
    elim (H2 a); intros.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
In a s2
    assert (In a s).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
In a s
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
In a s2
     eapply filter_1; eauto.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
In a s2
    elim H3; intros; auto.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
In a s2
    absurd (f a = true).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
f a <> true
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
f a = true
    intro.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
H7:f a = true
False
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
f a = true
    generalize (filter_2 D H1).s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
H7:f a = true
negb (f a) = true -> False
s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
f a = true
    rewrite H7; intros H8; inversion H8.s:t
f:elt -> bool
s1, s2:t
C:compat_bool E.eq f
D:compat_bool E.eq (fun x : E.t => negb (f x))
H0:For_all (fun x : elt => f x = true) s1
H:For_all (fun x : elt => f x = true -> False) s2
H2:forall x : elt, In x s <-> In x s1 \/ In x s2
a:elt
H1:In a (filter (fun x : elt => negb (f x)) s)
H3:In a s -> In a s1 \/ In a s2
H4:In a s1 \/ In a s2 -> In a s
H5:In a s
H6:In a s1
f a = true
    exact (H0 a H6).
  Qed.


  Definition elt := elt.
  Definition t := t.

  Definition In := In.
  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
  Definition Subset s s' := forall a : elt, In a s -> In a s'.
  Definition Add (x : elt) (s s' : t) :=
    forall y : elt, In y s' <-> E.eq y x \/ In y s.
  Definition Empty s := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) (s : t) :=
    forall x : elt, In x s -> P x.
  Definition Exists (P : elt -> Prop) (s : t) :=
    exists x : elt, In x s /\ P x.

  Definition In_1 := eq_In.

  Definition eq := Equal.
  Definition lt := lt.
  Definition eq_refl := eq_refl.
  Definition eq_sym := eq_sym.
  Definition eq_trans := eq_trans.
  Definition lt_trans := lt_trans.
  Definition lt_not_eq := lt_not_eq.
  Definition compare := compare.

  Module E := E.

End NodepOfDep.