Require Import Recdef.
Require Import NArith.
Require Import Sorting.
Require Import GeoCoq.Tactics.Coinc.Permutations.
Require Import GeoCoq.Utils.general_tactics.
Require Import GeoCoq.Utils.sets.

Module SSWP := WPropertiesOn SetOfSetsOfPositiveOrderedType SS.

Module SSWEqP := WEqPropertiesOn SetOfSetsOfPositiveOrderedType SS.

Module Import PosSort := Sort PosOrder.

Section Coinc_refl.

Context {AR : Arity}.

Definition pick_variety_auxCP {m : nat} (s : SS.elt) (cp : cartesianPower positive (S (S m))) : bool.
Proof.
(* Goal: SS.elt *)
induction m.
(* Goal: bool *)
(* Goal: bool *)
exact ((S.mem (fst cp) s) && (S.mem (snd cp) s)).
(* Goal: bool *)
exact ((S.mem (fst cp) s) && (IHm (tailCP cp))).
Defined.

Definition pick_variety_aux (s : SS.elt) (t : tST) := pick_variety_auxCP s t.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma pick_variety_auxCP_forallT {m : nat} :
  forall s (cp : cartesianPower positive (S (S m))),
  pick_variety_auxCP s cp = true <-> (forall p, InCP p cp -> S.mem p s = true).
Proof.
induction m; intros s cp; [unfold InCP|]; simpl; split.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  intro Hmem; apply andb_true_iff in Hmem; destruct Hmem as [Hmem1 Hmem2].
  intros p H; do 2 (try (elim H; clear H; intro; subst)); auto.
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  intro H; apply andb_true_iff; split;
  [apply (H (fst cp))|apply (H (snd cp))]; auto.
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  intro Hmem; apply andb_true_iff in Hmem; destruct Hmem as [Hmem1 Hmem2].
  intros p H; apply InCPOK in H; elim H; clear H; intro HIn; subst; simpl; auto.
  destruct (IHm s (tailCP cp)) as [H _]; apply H; auto.
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  destruct (IHm s (tailCP cp)) as [_ H]; clear IHm; rename H into IHm.
  intro H; apply andb_true_iff; split;
  [apply (H (fst cp))|apply IHm; intros p HIn; apply H]; apply InCPOK; auto.
  }
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma pick_variety_auxCP_existsF {m : nat} :
  forall s (cp : cartesianPower positive (S (S m))),
  pick_variety_auxCP s cp = false <-> (exists p, InCP p cp /\ S.mem p s = false).
Proof.
induction m; intros s cp; [unfold InCP|]; simpl; split.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  intro H; apply andb_false_iff in H; elim H; clear H; intro H;
  [exists (fst cp)|exists (snd cp)]; auto.
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  intro H; destruct H as [p [H Hmem]]; apply andb_false_iff.
  do 2 (try (elim H; clear H; intro H; subst)); intuition.
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  intro H; apply andb_false_iff in H.
  destruct (IHm s (tailCP cp)) as [H' _]; clear IHm; rename H' into IHm.
  elim H; clear H; intro Hmem.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
    {
    exists (fst cp); unfold InCP; simpl; auto.
    }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
    {
    destruct (IHm Hmem) as [p [HIn Hmem']]; exists p;
    split; try apply InCPOK; auto.
    }
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
  destruct (IHm s (tailCP cp)) as [_ H]; clear IHm; rename H into IHm.
  intro H; destruct H as [p [HIn Hmem]]; apply InCPOK in HIn; apply andb_false_iff.
  elim HIn; clear HIn; intro HIn; subst; auto.
  right; apply IHm; exists p; auto.
  }
Qed.

Lemma proper_00 :
  forall s,
  Proper
  ((fun (t1 t2 : tST) =>
     eqST t1 t2) ==> eq)
  (fun t : tST => pick_variety_aux s t).
Proof.
(* Goal: forall s : SS.elt, @Proper (forall _ : @tST AR, bool) (@respectful (@tST AR) bool (fun t1 t2 : @tST AR => @eqST AR t1 t2) (@eq bool)) (fun t : @tST AR => pick_variety_aux s t) *)
unfold pick_variety_aux, eqST.
(* Goal: forall s : SS.elt, @Proper (forall _ : @tST AR, bool) (@respectful (@tST AR) bool (fun t1 t2 : @tST AR => eqList (sets.PosSort.sort (@CPToList positive (S (S (@n AR))) t1)) (sets.PosSort.sort (@CPToList positive (S (S (@n AR))) t2))) (@eq bool)) (fun t : @tST AR => @pick_variety_auxCP (@n AR) s t) *)
intros s t1 t2 HEq.
(* Goal: @eq bool (@pick_variety_auxCP (@n AR) s t1) (@pick_variety_auxCP (@n AR) s t2) *)
case_eq (pick_variety_auxCP s t1); intro Ht1.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
(* Goal: @eq bool true (@pick_variety_auxCP (@n AR) s t2) *)
  destruct (pick_variety_auxCP_forallT s t1) as [H1 H2]; clear H2.
(* Goal: @eq bool false (@pick_variety_auxCP (@n AR) s t2) *)
  assert (H := H1 Ht1); clear H1; clear Ht1; rename H into Ht1.
(* Goal: @eq bool true (@pick_variety_auxCP (@n AR) s t2) *)
  destruct (pick_variety_auxCP_forallT s t2) as [H1 H2]; clear H1.
(* Goal: @eq bool true (@pick_variety_auxCP (@n AR) s t2) *)
  rewrite H2; try reflexivity; clear H2; intros p HIn; apply Ht1.
(* Goal: @InCP positive (S (S (@n AR))) p t1 *)
  clear Ht1; apply InCPOCP; apply InCPOCP in HIn.
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  assert (H : eqList (CPToList (OCP t1)) (CPToList (OCP t2))).
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
    {
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    assert (Ht1 := eqListSortOCP t1).
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    assert (Ht2 := eqListSortOCP t2).
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    apply eqListTrans with (PosSort.sort (CPToList t1)); try assumption.
(* Goal: eqList (sort (@CPToList positive (S (S (@n AR))) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    apply eqListTrans with (PosSort.sort (CPToList t2)); try assumption.
(* Goal: eqList (sort (@CPToList positive (S (S (@n AR))) t2)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    apply eqListSym; assumption.
    }
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  clear HEq; rename H into HEq; apply eqListOK in HEq.
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t1) *)
  unfold InCP in *; rewrite HEq; auto.
  }

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  {
(* Goal: @eq bool false (@pick_variety_auxCP (@n AR) s t2) *)
  destruct (pick_variety_auxCP_existsF s t1) as [H1 H2]; clear H2.
(* Goal: @eq bool false (@pick_variety_auxCP (@n AR) s t2) *)
  assert (H := H1 Ht1); clear H1; clear Ht1; rename H into Ht1.
(* Goal: @eq bool false (@pick_variety_auxCP (@n AR) s t2) *)
  destruct (pick_variety_auxCP_existsF s t2) as [H1 H2]; clear H1.
(* Goal: @eq bool false (@pick_variety_auxCP (@n AR) s t2) *)
  rewrite H2; try reflexivity; clear H2.
(* Goal: @ex positive (fun p : positive => and (@InCP positive (S (S (@n AR))) p t2) (@eq bool (S.mem p s) false)) *)
  destruct Ht1 as [p [HIn Hmem]]; exists p; split; auto.
(* Goal: @InCP positive (S (S (@n AR))) p t2 *)
  apply InCPOCP; apply InCPOCP in HIn.
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  assert (H : eqList (CPToList (OCP t1)) (CPToList (OCP t2))).
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
    {
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    assert (Ht1 := eqListSortOCP t1).
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    assert (Ht2 := eqListSortOCP t2).
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    apply eqListTrans with (PosSort.sort (CPToList t1)); try assumption.
(* Goal: eqList (sort (@CPToList positive (S (S (@n AR))) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    apply eqListTrans with (PosSort.sort (CPToList t2)); try assumption.
(* Goal: eqList (sort (@CPToList positive (S (S (@n AR))) t2)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
    apply eqListSym; assumption.
    }
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  clear HEq; rename H into HEq; apply eqListOK in HEq.
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
  unfold InCP in *; rewrite <- HEq; auto.
  }
Qed.

Definition pick_variety (s : SS.elt) (st : STt) :=
  STexists_ (fun t => pick_variety_aux s t) st.

Lemma proper_0 :
  Proper (S.Equal ==> eq ==> eq) pick_variety.
Proof.
(* Goal: @Proper (forall (_ : S.t) (_ : SS.t) (_ : @STt AR), option (prod SS.elt SS.elt)) (@respectful S.t (forall (_ : SS.t) (_ : @STt AR), option (prod SS.elt SS.elt)) S.Equal (@respectful SS.t (forall _ : @STt AR, option (prod SS.elt SS.elt)) SS.Equal (@respectful (@STt AR) (option (prod SS.elt SS.elt)) (@eq (@STt AR)) eqopp))) pick_varieties_aux *)
intros x1 y1 HXY1.
(* Goal: @respectful SS.t (forall _ : @STt AR, option (prod SS.elt SS.elt)) SS.Equal (@respectful (@STt AR) (option (prod SS.elt SS.elt)) (@eq (@STt AR)) eqopp) (pick_varieties_aux x1) (pick_varieties_aux y1) *)
intros x2 y2 HXY2.
(* Goal: @eq bool (pick_variety x1 x2) (pick_variety y1 y2) *)
rewrite HXY2; clear HXY2; clear x2.
(* Goal: @eq bool (pick_variety x1 y2) (pick_variety y1 y2) *)
unfold pick_variety; unfold pick_variety_aux.
(* Goal: @eq bool (@STexists_ AR (fun t : @STelt AR => @pick_variety_auxCP (@n AR) x1 t) y2) (@STexists_ AR (fun t : @STelt AR => @pick_variety_auxCP (@n AR) y1 t) y2) *)
unfold STexists_.

(* Goal: @eq bool ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => @pick_variety_auxCP (@n AR) x1 t) y2) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => @pick_variety_auxCP (@n AR) y1 t) y2) *)
  induction y2; try reflexivity.

(* Goal: @eq bool (orb (@pick_variety_auxCP (@n AR) x1 a) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => @pick_variety_auxCP (@n AR) x1 t) y2)) (orb (@pick_variety_auxCP (@n AR) y1 a) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => @pick_variety_auxCP (@n AR) y1 t) y2)) *)
    rewrite IHy2; clear IHy2.
    assert (HEqMem : forall e, S.mem e x1 = S.mem e y1)
      by (intro; apply SWP.Dec.F.mem_m; intuition); clear HXY1.
    assert (HF : forall n a,
               (fix F (n : nat) : cartesianPower positive (S (S n)) -> bool :=
                 match n as n0 return (cartesianPower positive (S (S n0)) -> bool) with
                 | 0 => fun t0 : cartesianPower positive 2 => S.mem (fst t0) x1 && S.mem (snd t0) x1
                 | S n0 => fun t0 : cartesianPower positive (S (S (S n0))) =>
                             S.mem (headCP t0) x1 && F n0 (tailCP t0)
                 end) n a =
               (fix F (n : nat) : cartesianPower positive (S (S n)) -> bool :=
                  match n as n0 return (cartesianPower positive (S (S n0)) -> bool) with
                  | 0 => fun t0 : cartesianPower positive 2 => S.mem (fst t0) y1 && S.mem (snd t0) y1
                  | S n0 => fun t0 : cartesianPower positive (S (S (S n0))) =>
                              S.mem (headCP t0) y1 && F n0 (tailCP t0)
                  end) n a)
      by (induction n; try (intro; do 2 (rewrite HEqMem); reflexivity);
          intro ; rewrite HEqMem; rewrite IHn; reflexivity).
(* Goal: @eq bool (orb (@pick_variety_auxCP (@n AR) x1 a) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => @pick_variety_auxCP (@n AR) y1 t) y2)) (orb (@pick_variety_auxCP (@n AR) y1 a) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => @pick_variety_auxCP (@n AR) y1 t) y2)) *)
    unfold pick_variety_auxCP.
(* Goal: @eq bool (orb (nat_rect (fun m : nat => forall _ : cartesianPower positive (S (S m)), bool) (fun cp : cartesianPower positive (S (S O)) => andb (S.mem (@fst positive positive cp) x1) (S.mem (@snd positive positive cp) x1)) (fun (m : nat) (IHm : forall _ : cartesianPower positive (S (S m)), bool) (cp : cartesianPower positive (S (S (S m)))) => andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) x1) (IHm (@tailCP positive (S m) cp))) (@n AR) a) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => nat_rect (fun m : nat => forall _ : cartesianPower positive (S (S m)), bool) (fun cp : cartesianPower positive (S (S O)) => andb (S.mem (@fst positive positive cp) y1) (S.mem (@snd positive positive cp) y1)) (fun (m : nat) (IHm : forall _ : cartesianPower positive (S (S m)), bool) (cp : cartesianPower positive (S (S (S m)))) => andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) y1) (IHm (@tailCP positive (S m) cp))) (@n AR) t) y2)) (orb (nat_rect (fun m : nat => forall _ : cartesianPower positive (S (S m)), bool) (fun cp : cartesianPower positive (S (S O)) => andb (S.mem (@fst positive positive cp) y1) (S.mem (@snd positive positive cp) y1)) (fun (m : nat) (IHm : forall _ : cartesianPower positive (S (S m)), bool) (cp : cartesianPower positive (S (S (S m)))) => andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) y1) (IHm (@tailCP positive (S m) cp))) (@n AR) a) ((fix STexists_ (f : forall _ : @STelt AR, bool) (s : @STt AR) {struct s} : bool := match s with | nil => false | cons hd tl => orb (f hd) (STexists_ f tl) end) (fun t : @STelt AR => nat_rect (fun m : nat => forall _ : cartesianPower positive (S (S m)), bool) (fun cp : cartesianPower positive (S (S O)) => andb (S.mem (@fst positive positive cp) y1) (S.mem (@snd positive positive cp) y1)) (fun (m : nat) (IHm : forall _ : cartesianPower positive (S (S m)), bool) (cp : cartesianPower positive (S (S (S m)))) => andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) y1) (IHm (@tailCP positive (S m) cp))) (@n AR) t) y2)) *)
    rewrite HF; reflexivity.
Qed.

Lemma proper_1 : forall s1 st,
  Proper (S.Equal ==> eq)
  (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st).
Proof.
(* Goal: forall (s1 : S.t) (st : @STt AR), @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) *)
intros s1 st.
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) (SS.remove s1 ss)) (@Some SS.elt s2) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
intros x y HXY.
assert (HEqI : S.Equal (S.inter s1 x) (S.inter s1 y))
  by (apply SWP.inter_equal_2; assumption).
(* Goal: @eq bool (pick_variety (S.inter s1 x) st) (pick_variety (S.inter s1 y) st) *)
apply proper_0; auto.
Qed.

Definition exists_witness (f : SS.elt -> bool) (s : SS.t) : option SS.elt :=
  SS.choose (SS.filter f s).

Lemma exists_witness_ok : forall e f s,
  Proper (S.Equal ==> eq) f ->
  exists_witness f s = Some e -> SS.In e s.
Proof.
(* Goal: forall (e : SS.elt) (f : forall _ : S.t, bool) (s : SS.t) (_ : @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) f) (_ : @eq (option SS.elt) (exists_witness f s) (@Some SS.elt e)), SS.In e s *)
intros e f s HP H.
(* Goal: SS.In e s *)
unfold exists_witness in H.
(* Goal: SS.In e s *)
apply SSWEqP.MP.Dec.F.mem_2.
(* Goal: @eq bool (SS.mem e s) true *)
apply SSWEqP.choose_mem_1 in H.
(* Goal: @eq bool (SS.mem e s) true *)
rewrite SSWEqP.filter_mem in H; try assumption.
(* Goal: @eq bool (SS.mem e s) true *)
apply andb_true_iff in H.
(* Goal: @eq bool (SS.mem e s) true *)
induction H.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
assumption.
Qed.

Definition pick_varieties_aux (s1 : SS.elt) (ss : SS.t) (st : STt)
                              : (option (SS.elt * SS.elt)) :=
  match ((exists_witness (fun s2 => let i := S.inter s1 s2 in
                                    pick_variety i st)) ss) with
    | None => None
    | Some s2 => Some(s1,s2)
  end.

Definition pick_varieties (ss : SS.t) (st : STt)
                          : (option (SS.elt * SS.elt)) :=
  match (exists_witness (fun s =>
                           match (pick_varieties_aux s (SS.remove s ss) st) with
                             | None => false
                             | _ => true
                           end) ss) with
    | None => None
    | Some s1 => pick_varieties_aux s1 (SS.remove s1 ss) st
  end.

Definition eqop (p1 p2 : option SS.elt) :=
  match p1,p2 with
    | None, None => True
    | Some s1, Some s2 => True
    | _, _ => False
  end.

Lemma proper_2 : forall (f1 f2 : SS.elt -> bool) (s1 s2 : SS.t),
  Proper (S.Equal ==> eq) f1 ->
  Proper (S.Equal ==> eq) f2 ->
  (forall x, f1 x = f2 x) ->
  SS.Equal s1 s2 ->
  eqop (exists_witness f1 s1) (exists_witness f2 s2).
Proof.
intros f1 f2 s1 s2.
intros H1 H2 H3 H4.
unfold eqop.
unfold exists_witness in *.
assert (SS.Equal (SS.filter f1 s1) (SS.filter f2 s2)) by (apply SSWEqP.MP.Dec.F.filter_ext; assumption).
case_eq (SS.choose (SS.filter f1 s1)); case_eq (SS.choose (SS.filter f2 s2)).

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  intuition.

(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@Some SS.elt e)), eqopp (@None (prod SS.elt SS.elt)) (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 e)) *)
(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@Some SS.elt e)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 e)) (@None (prod SS.elt SS.elt)) *)
(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@None (prod SS.elt SS.elt)) (@None (prod SS.elt SS.elt)) *)
  intros HCN e HCS.
  apply SS.choose_spec1 in HCS.
  apply SS.choose_spec2 in HCN.
  rewrite H in HCS.
  apply SSWEqP.MP.empty_is_empty_1 in HCN.
  rewrite HCN in HCS.
  rewrite <- SSWEqP.MP.Dec.F.empty_iff.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  eassumption.

(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@Some SS.elt e)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 e)) (@None (prod SS.elt SS.elt)) *)
(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@None (prod SS.elt SS.elt)) (@None (prod SS.elt SS.elt)) *)
  intros e HCS HCN.
  apply SS.choose_spec1 in HCS.
  apply SS.choose_spec2 in HCN.
  rewrite H in HCN.
  apply SSWEqP.MP.empty_is_empty_1 in HCN.
  rewrite HCN in HCS.
  rewrite <- SSWEqP.MP.Dec.F.empty_iff.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  eassumption.

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  intuition.
Qed.

Definition eqopp (p1 p2 : option (SS.elt * SS.elt)) :=
  match p1,p2 with
    | None, None => True
    | Some s1, Some s2 => True
    | _, _ => False
  end.

Lemma proper_3 : Proper (S.Equal ==> SS.Equal ==> eq ==> eqopp) pick_varieties_aux.
Proof.
(* Goal: @Proper (forall (_ : S.t) (_ : SS.t) (_ : @STt AR), option (prod SS.elt SS.elt)) (@respectful S.t (forall (_ : SS.t) (_ : @STt AR), option (prod SS.elt SS.elt)) S.Equal (@respectful SS.t (forall _ : @STt AR, option (prod SS.elt SS.elt)) SS.Equal (@respectful (@STt AR) (option (prod SS.elt SS.elt)) (@eq (@STt AR)) eqopp))) pick_varieties_aux *)
intros x1 y1 HXY1.
(* Goal: @respectful SS.t (forall _ : @STt AR, option (prod SS.elt SS.elt)) SS.Equal (@respectful (@STt AR) (option (prod SS.elt SS.elt)) (@eq (@STt AR)) eqopp) (pick_varieties_aux x1) (pick_varieties_aux y1) *)
intros x2 y2 HXY2.
(* Goal: @respectful (@STt AR) (option (prod SS.elt SS.elt)) (@eq (@STt AR)) eqopp (pick_varieties_aux x1 x2) (pick_varieties_aux y1 y2) *)
intros x3 y3 HXY3.
(* Goal: eqopp (pick_varieties_aux x1 x2 x3) (pick_varieties_aux y1 y2 y3) *)
unfold pick_varieties_aux.
(* Goal: eqopp match exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) x3) x2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 s2) | None => @None (prod SS.elt SS.elt) end match exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 s2) | None => @None (prod SS.elt SS.elt) end *)
rewrite HXY3.
assert (eqop (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2)
             (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2)).

(* Goal: eqop (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) *)
(* Goal: eqopp match exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 s2) | None => @None (prod SS.elt SS.elt) end match exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 s2) | None => @None (prod SS.elt SS.elt) end *)
  apply proper_2.

(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) *)
(* Goal: forall x : SS.elt, @eq bool (pick_variety (S.inter x1 x) y3) (pick_variety (S.inter y1 x) y3) *)
(* Goal: SS.Equal x2 y2 *)
(* Goal: eqopp match exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 s2) | None => @None (prod SS.elt SS.elt) end match exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 s2) | None => @None (prod SS.elt SS.elt) end *)
    apply proper_1.

(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) *)
(* Goal: forall x : SS.elt, @eq bool (pick_variety (S.inter x1 x) y3) (pick_variety (S.inter y1 x) y3) *)
(* Goal: SS.Equal x2 y2 *)
(* Goal: eqopp match exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 s2) | None => @None (prod SS.elt SS.elt) end match exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 s2) | None => @None (prod SS.elt SS.elt) end *)
    apply proper_1.

(* Goal: forall x : SS.elt, @eq bool (pick_variety (S.inter x1 x) y3) (pick_variety (S.inter y1 x) y3) *)
(* Goal: SS.Equal x2 y2 *)
(* Goal: eqopp match exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 s2) | None => @None (prod SS.elt SS.elt) end match exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 s2) | None => @None (prod SS.elt SS.elt) end *)
    intro; apply proper_0; try reflexivity.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply SWP.inter_equal_1; assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      assumption.

case_eq (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2);
case_eq (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2).

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl; intuition.

(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@Some SS.elt e)), eqopp (@None (prod SS.elt SS.elt)) (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 e)) *)
(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@Some SS.elt e)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 e)) (@None (prod SS.elt SS.elt)) *)
(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@None (prod SS.elt SS.elt)) (@None (prod SS.elt SS.elt)) *)
  intros HCN e HCS.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl in *.
(* Goal: False *)
(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@None (prod SS.elt SS.elt)) (@None (prod SS.elt SS.elt)) *)
  rewrite HCS in H; rewrite HCN in H.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl in *.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  intuition.

(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@Some SS.elt e)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 e)) (@None (prod SS.elt SS.elt)) *)
(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@None (prod SS.elt SS.elt)) (@None (prod SS.elt SS.elt)) *)
  intros e HCS HCN.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl in *.
(* Goal: False *)
(* Goal: forall (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2) (@None SS.elt)) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2) (@None SS.elt)), eqopp (@None (prod SS.elt SS.elt)) (@None (prod SS.elt SS.elt)) *)
  rewrite HCS in H; rewrite HCN in H.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl in *.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  intuition.

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  intuition.
Qed.

Lemma pick_varieties_ok_1 : forall s1 s2 ss st,
  pick_varieties ss st = Some(s1,s2) ->
  SS.In s1 ss.
Proof.
(* Goal: forall (s1 s2 : SS.elt) (ss : SS.t) (st : @STt AR) (_ : @eq (option (prod SS.elt SS.elt)) (pick_varieties ss st) (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt s1 s2))), SS.In s2 (SS.remove s1 ss) *)
intros s1 s2 ss st H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
unfold pick_varieties in H.
case_eq (exists_witness (fun s : SS.elt => match pick_varieties_aux s
                          (SS.remove s ss) st with | Some _ => true | None => false end) ss).

(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt e)), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  intros e1 HEW1.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  rewrite HEW1 in H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  unfold pick_varieties_aux in H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  case_eq (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)).

(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@Some SS.elt e)), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    intros e2 HEW2.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEW2 in H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    assert (HEq1 : e1 = s1) by (injection H; intros; assumption).
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEq1 in *.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    assert (HEq2 : e2 = s2) by (injection H; intros; assumption).
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEq2 in *.
    apply exists_witness_ok with (fun s : SS.elt =>
      match pick_varieties_aux s (SS.remove s ss) st with | Some _ => true | None => false end).
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) (SS.remove s1 ss)) (@Some SS.elt s2) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    intros x y HXY.
    assert (SS.Equal (SS.remove x ss) (SS.remove y ss))
      by (apply SSWP.Dec.F.remove_m; try assumption; reflexivity).
    assert (eqopp (pick_varieties_aux x (SS.remove x ss) st) (pick_varieties_aux y (SS.remove y ss) st))
      by (apply proper_3; auto).
    case_eq (pick_varieties_aux x (SS.remove x ss) st);
      intros;
      case_eq (pick_varieties_aux y (SS.remove y ss) st);
(* Goal: forall interp : forall _ : positive, @COINCpoint AR, st_ok (@STempty AR) interp *)
      intros.

(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
      reflexivity.

(* Goal: @eq bool false true *)
(* Goal: @eq bool false false *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt s1) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s1 ss *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s1 ss *)
      rewrite H2 in H1; rewrite H3 in H1.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false false *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt s1) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s1 ss *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s1 ss *)
      unfold eqop in H1; simpl in H1.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
      intuition.

(* Goal: @eq bool false true *)
(* Goal: @eq bool false false *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt s1) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s1 ss *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s1 ss *)
      rewrite H2 in H1; rewrite H3 in H1.
(* Goal: @eq bool false true *)
(* Goal: @eq bool false false *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt s1) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s1 ss *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s1 ss *)
      unfold eqop in H1; simpl in H1.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
      intuition.

(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
      reflexivity.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.

(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    intro HEW2.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEW2 in H.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
    discriminate.

(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  intro HEW.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
  rewrite HEW in H.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
  discriminate.
Qed.

Lemma pick_varieties_ok_2 : forall s1 s2 ss st,
  pick_varieties ss st = Some(s1,s2) ->
  SS.In s2 (SS.remove s1 ss).
Proof.
(* Goal: forall (s1 s2 : SS.elt) (ss : SS.t) (st : @STt AR) (_ : @eq (option (prod SS.elt SS.elt)) (pick_varieties ss st) (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt s1 s2))), SS.In s2 (SS.remove s1 ss) *)
intros s1 s2 ss st H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
unfold pick_varieties in H.
case_eq (exists_witness (fun s : SS.elt => match pick_varieties_aux s
                          (SS.remove s ss) st with | Some _ => true | None => false end) ss).

(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt e)), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  intros e1 HEW1.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  rewrite HEW1 in H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  unfold pick_varieties_aux in H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  case_eq (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)).

(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@Some SS.elt e)), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    intros e2 HEW2.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEW2 in H.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    assert (HEq1 : e1 = s1) by (injection H; intros; assumption).
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEq1 in *.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    assert (HEq2 : e2 = s2) by (injection H; intros; assumption).
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEq2 in *.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    apply exists_witness_ok with (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st).
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) *)
(* Goal: @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter s1 s2) st) (SS.remove s1 ss)) (@Some SS.elt s2) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    intros x y HXY.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply proper_1; assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.

(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    intro HEW2.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
    rewrite HEW2 in H.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
    discriminate.

(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
  intro HEW.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
  rewrite HEW in H.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
  discriminate.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Function identify_varieties (ss : SS.t) (st : STt) {measure SS.cardinal ss}
                                 : SS.t :=
  let varieties := pick_varieties ss st in
    match varieties with
      |None => ss
      |Some (s1,s2) => let auxsetofsets := SS.remove s2 (SS.remove s1 ss) in
                       let auxset := S.union s1 s2 in
                       let newss := SS.add auxset auxsetofsets in
                         identify_varieties newss st
    end.
Proof.
(* Goal: forall interp : forall _ : positive, @COINCpoint AR, st_ok (@STempty AR) interp *)
intros.
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
assert (S(SS.cardinal (SS.remove s1 ss)) = SS.cardinal ss).
(* Goal: @eq nat (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal (SS.remove s1 ss)) *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
apply SSWP.remove_cardinal_1.
(* Goal: SS.In s1 ss *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
apply pick_varieties_ok_1 with s2 st.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
assumption.
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
assert (S(S(SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) = S(SS.cardinal (SS.remove s1 ss))).
(* Goal: @eq nat (S (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss))))) (S (SS.cardinal (SS.remove s1 ss))) *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
apply eq_S.
(* Goal: @eq nat (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal (SS.remove s1 ss)) *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
apply SSWP.remove_cardinal_1.
(* Goal: SS.In s2 (SS.remove s1 ss) *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
apply pick_varieties_ok_2 with st.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
assumption.
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
assert (HR1 : S(S(SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) = SS.cardinal ss).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
transitivity (S(SS.cardinal (SS.remove s1 ss))); assumption.
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
elim (SSWP.In_dec (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss))); intro HDec.

(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  assert (HR2 : SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss))) = SS.cardinal (SS.remove s2 (SS.remove s1 ss))).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply SSWP.add_cardinal_1; assumption.
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  rewrite HR2.
(* Goal: lt (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  rewrite <- HR1.
(* Goal: lt (SS.cardinal (SS.remove s2 (SS.remove s1 ss))) (S (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss))))) *)
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  apply le_S;apply le_n.

(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  assert (HR2 : SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss))) = S( SS.cardinal (SS.remove s2 (SS.remove s1 ss)))).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply SSWP.add_cardinal_2; assumption.
(* Goal: lt (SS.cardinal (SS.add (S.union s1 s2) (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  rewrite HR2.
(* Goal: lt (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) (SS.cardinal ss) *)
  rewrite <- HR1.
(* Goal: lt (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss)))) (S (S (SS.cardinal (SS.remove s2 (SS.remove s1 ss))))) *)
  apply le_n.
Defined.

Definition memCPAux m (cp : cartesianPower positive (S (S m))) (s : SS.elt) : bool.
Proof.
(* Goal: SS.elt *)
induction m.
(* Goal: bool *)
(* Goal: bool *)
exact (S.mem (fst cp) s && S.mem (snd cp) s).
(* Goal: bool *)
exact (S.mem (fst cp) s && (IHm (snd cp))).
Defined.

Lemma memCPAuxHdTl : forall m cp s,
  memCPAux (S m) cp s = S.mem (fst cp) s && memCPAux m (tailCP cp) s.
Proof.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
induction m; unfold memCPAux; unfold nat_rect; reflexivity.
Qed.

Lemma memCPAuxProperOK : forall m, Proper (eq ==> S.Equal==> eq) (memCPAux m).
Proof.
(* Goal: forall m : nat, @Proper (forall (_ : cartesianPower positive (S (S m))) (_ : S.t), bool) (@respectful (cartesianPower positive (S (S m))) (forall _ : S.t, bool) (@eq (cartesianPower positive (S (S m)))) (@respectful S.t bool S.Equal (@eq bool))) (memCPAux m) *)
intros m cp1 cp2 Hcp s1 s2 Hs.
(* Goal: @eq bool (memCPAux m cp1 s1) (memCPAux m cp2 s2) *)
rewrite Hcp; clear Hcp; clear cp1; rename cp2 into cp.
(* Goal: forall (cp : cartesianPower S.elt (S (S O))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S O)) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux O cp s) true *)
(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
unfold memCPAux.
(* Goal: @eq bool (nat_rect (fun m : nat => forall _ : cartesianPower positive (S (S m)), bool) (fun cp : cartesianPower positive (S (S O)) => andb (S.mem (@fst positive positive cp) s1) (S.mem (@snd positive positive cp) s1)) (fun (m : nat) (IHm : forall _ : cartesianPower positive (S (S m)), bool) (cp : cartesianPower positive (S (S (S m)))) => andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s1) (IHm (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp))) m cp) (nat_rect (fun m : nat => forall _ : cartesianPower positive (S (S m)), bool) (fun cp : cartesianPower positive (S (S O)) => andb (S.mem (@fst positive positive cp) s2) (S.mem (@snd positive positive cp) s2)) (fun (m : nat) (IHm : forall _ : cartesianPower positive (S (S m)), bool) (cp : cartesianPower positive (S (S (S m)))) => andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) (IHm (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp))) m cp) *)
assert (H : forall p, S.mem p s1 = S.mem p s2) by (intro p; apply SWP.Dec.F.mem_m; trivial).
(* Goal: SS.elt *)
induction m.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
simpl; do 2 (rewrite H); reflexivity.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
simpl; rewrite H; rewrite IHm; reflexivity.
Qed.

Lemma memCPAuxOK : forall m cp s e,
  memCPAux m cp s = true -> InCP e cp -> S.mem e s = true.
Proof.
(* Goal: SS.elt *)
induction m.

(* Goal: forall (cp : cartesianPower S.elt (S (S O))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S O)) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux O cp s) true *)
(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
  unfold memCPAux.
  intros cp s e Hmem HIn.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  unfold InCP in HIn.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl in *.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  rewrite andb_true_iff in Hmem.
  do 2 (elim HIn; clear HIn; intro HIn; try (subst; spliter; auto)).

  intros cp s e Hmem HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
  apply InCPOK in HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
  elim HIn; clear HIn; intro HIn.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    subst.
    simpl in Hmem.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
    rewrite andb_true_iff in Hmem.
    spliter.
    auto.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply IHm with (tailCP cp); try assumption.
    simpl in Hmem.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
    rewrite andb_true_iff in Hmem.
    spliter.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.
Qed.

Lemma memMemCPAuxOK : forall m cp s,
  (forall e, InCP e cp -> S.mem e s = true) -> memCPAux m cp s = true.
Proof.
(* Goal: SS.elt *)
induction m.

(* Goal: forall (cp : cartesianPower S.elt (S (S O))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S O)) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux O cp s) true *)
(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
  unfold memCPAux.
(* Goal: and (@eq positive (@headCP positive (S (S (@length positive l))) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e)) e) (@eq positive (@headCP positive (S (@length positive l)) (@tailCP positive (S (@length positive l)) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e))) e) *)
  simpl.
(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
  intros cp s H.
(* Goal: @eq bool (andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s) (memCPAux m (@tailCP positive (S m) cp) s)) true *)
  rewrite andb_true_iff.
(* Goal: and (@eq bool (S.mem (@fst positive positive cp) s) true) (@eq bool (S.mem (@snd positive positive cp) s) true) *)
(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
  assert (HIn1 : InCP (fst cp) cp) by (unfold InCP; simpl; auto).
(* Goal: and (@eq bool (S.mem (@fst positive positive cp) s) true) (@eq bool (S.mem (@snd positive positive cp) s) true) *)
(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
  assert (HIn2 : InCP (snd cp) cp) by (unfold InCP; simpl; auto).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  split; apply H; assumption.

(* Goal: forall (cp : cartesianPower S.elt (S (S (S m)))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S m))) e cp), @eq bool (S.mem e s) true), @eq bool (memCPAux (S m) cp s) true *)
  intros cp s H.
(* Goal: @eq bool (memCPAux (S m) cp s) true *)
  rewrite memCPAuxHdTl.
(* Goal: @eq bool (andb (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s) (memCPAux m (@tailCP positive (S m) cp) s)) true *)
  rewrite andb_true_iff.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s) true) (@eq bool (memCPAux m (@tailCP positive (S m) cp) s) true) *)
  assert (HIn : InCP (fst cp) cp) by (unfold InCP; simpl; auto).
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s) true) (@eq bool (memCPAux m (@tailCP positive (S m) cp) s) true) *)
  split; try (apply H; assumption); clear HIn.
(* Goal: @InCP S.elt (S m) e (@tailCP S.elt m cp) *)
  apply IHm.
(* Goal: forall (e : S.elt) (_ : @InCP S.elt (S (S (S (@n AR)))) e (@consHeadCP S.elt (S (S (@n AR))) p x)), @eq bool (S.mem e s) true *)
  intros e HIn.
(* Goal: @eq bool (S.mem e s) true *)
  apply H.
(* Goal: @InCP S.elt (S (S m)) e cp *)
  apply InCPOK.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  right.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  assumption.
Qed.

Lemma memCPAuxTlOK : forall m cp s,
  memCPAux (S m) cp s = true ->
  memCPAux m (tailCP cp) s = true.
Proof.
(* Goal: forall (m : nat) (cp : cartesianPower positive (S (S (S m)))) (s : SS.elt) (_ : @eq bool (memCPAux (S m) cp s) true), @eq bool (memCPAux m (@tailCP positive (S m) cp) s) true *)
intros m cp s Hmemcp.
(* Goal: forall (cp : cartesianPower S.elt (S (S (S (@n AR))))) (s : S.t) (_ : forall (e : S.elt) (_ : @InCP S.elt (S (S (S (@n AR)))) e cp), @eq bool (S.mem e s) true), @eq bool (memCP cp s) true *)
apply memMemCPAuxOK.
(* Goal: forall (e : S.elt) (_ : @InCP S.elt (S (S (S (@n AR)))) e (@consHeadCP S.elt (S (S (@n AR))) p x)), @eq bool (S.mem e s) true *)
intros e HIn.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply memCPAuxOK with (S m) cp; try assumption.
(* Goal: @InCP S.elt (S (S m)) e cp *)
apply InCPOK.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
right; assumption.
Qed.

Definition memCP (cp : cartesianPower positive (S (S (S n)))) (s : SS.elt) := memCPAux (S n) cp s.

Lemma memCPProper : Proper (eq ==> S.Equal==> eq) memCP.
Proof. apply memCPAuxProperOK. Qed.

Lemma memMemCPOK : forall cp s,
  (forall e, InCP e cp -> S.mem e s = true) -> memCP cp s = true.
Proof. apply memMemCPAuxOK. Qed.

Lemma memCPConsHd : forall p s x,
  S.mem p s = true ->
  memCPAux n x s = true ->
  memCP (consHeadCP p x) s = true.
Proof.
(* Goal: forall (p : S.elt) (s : S.t) (x : cartesianPower positive (S (S (@n AR)))) (_ : @eq bool (S.mem p s) true) (_ : @eq bool (memCPAux (@n AR) x s) true), @eq bool (memCP (@consHeadCP S.elt (S (S (@n AR))) p x) s) true *)
intros p s x Hmem Hmemcp.
(* Goal: @eq bool (memCP (@consHeadCP S.elt (S (S (@n AR))) p x) s) true *)
apply memMemCPOK.
(* Goal: forall (e : S.elt) (_ : @InCP S.elt (S (S (S (@n AR)))) e (@consHeadCP S.elt (S (S (@n AR))) p x)), @eq bool (S.mem e s) true *)
intros e HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
apply InCPOK in HIn.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
simpl in HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
elim HIn; clear HIn; intro HIn.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  subst; assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply memCPAuxOK with n x; assumption.
Qed.

Definition test_coinc (ss : SS.t) (st : STt) (cp : cartesianPower positive (S (S (S n)))) : bool :=
  let newss := identify_varieties ss st  in
    SS.exists_ (fun s => memCP cp s) newss.

Lemma pick_variety_aux_memCPAux1 : forall s1 s2 m (cp : cartesianPower positive (S (S m))),
  pick_variety_auxCP (S.inter s1 s2) cp = true ->
  memCPAux m cp s1 = true.
Proof.
(* Goal: forall (s1 s2 : S.t) (m : nat) (cp : cartesianPower positive (S (S m))) (_ : @eq bool (@pick_variety_auxCP m (S.inter s1 s2) cp) true), @eq bool (memCPAux m cp s2) true *)
intros s1 s2 m cp.
(* Goal: forall _ : @eq bool (@pick_variety_auxCP m (S.inter s1 s2) cp) true, @eq bool (memCPAux m cp s2) true *)
induction m; simpl; do 2 (rewrite andb_true_iff); intro Hhtspa.

(* Goal: and (@eq bool (S.mem (@fst positive positive cp) s2) true) (@eq bool (S.mem (@snd positive positive cp) s2) true) *)
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  do 2 (rewrite SWP.FM.inter_b in Hhtspa).
(* Goal: and (@eq bool (S.mem (@fst positive positive cp) s2) true) (@eq bool (S.mem (@snd positive positive cp) s2) true) *)
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  do 2 (rewrite andb_true_iff in Hhtspa).
  tauto.

(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  destruct Hhtspa as [Hmem Hhtspa].
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  rewrite SWP.FM.inter_b in Hmem.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  rewrite andb_true_iff in Hmem.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  split; try (spliter; assumption).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply IHm; assumption.
Qed.

Lemma pick_variety_aux_memCPAux2 : forall s1 s2 m (cp : cartesianPower positive (S (S m))),
  pick_variety_auxCP (S.inter s1 s2) cp = true ->
  memCPAux m cp s2 = true.
Proof.
(* Goal: forall (s1 s2 : S.t) (m : nat) (cp : cartesianPower positive (S (S m))) (_ : @eq bool (@pick_variety_auxCP m (S.inter s1 s2) cp) true), @eq bool (memCPAux m cp s2) true *)
intros s1 s2 m cp.
(* Goal: forall _ : @eq bool (@pick_variety_auxCP m (S.inter s1 s2) cp) true, @eq bool (memCPAux m cp s2) true *)
induction m; simpl; do 2 (rewrite andb_true_iff); intro Hhtspa.

(* Goal: and (@eq bool (S.mem (@fst positive positive cp) s2) true) (@eq bool (S.mem (@snd positive positive cp) s2) true) *)
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  do 2 (rewrite SWP.FM.inter_b in Hhtspa).
(* Goal: and (@eq bool (S.mem (@fst positive positive cp) s2) true) (@eq bool (S.mem (@snd positive positive cp) s2) true) *)
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  do 2 (rewrite andb_true_iff in Hhtspa).
  tauto.

(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  destruct Hhtspa as [Hmem Hhtspa].
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  rewrite SWP.FM.inter_b in Hmem.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  rewrite andb_true_iff in Hmem.
(* Goal: and (@eq bool (S.mem (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) (@eq bool (memCPAux m (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive m)) cp) s2) true) *)
  split; try (spliter; assumption).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply IHm; assumption.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Definition interp_CP {m : nat} (cp : cartesianPower positive (S m)) (interp: positive -> COINCpoint) : cartesianPower COINCpoint (S m).
Proof.
(* Goal: SS.elt *)
induction m.
(* Goal: cartesianPower (@COINCpoint AR) (S O) *)
(* Goal: cartesianPower (@COINCpoint AR) (S (S m)) *)
exact (interp cp).
(* Goal: cartesianPower (@COINCpoint AR) (S (S m)) *)
clear IHm.
(* Goal: SS.elt *)
induction m.
(* Goal: and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) (@pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) *)
split.
(* Goal: @COINCpoint AR *)
(* Goal: cartesianPowerAux (@COINCpoint AR) (S m) *)
exact (interp (headCP cp)).
(* Goal: cartesianPowerAux (@COINCpoint AR) O *)
(* Goal: cartesianPower (@COINCpoint AR) (S (S (S m))) *)
exact (interp (tailCP cp)).
(* Goal: and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) (@pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) *)
split.
(* Goal: @COINCpoint AR *)
(* Goal: cartesianPowerAux (@COINCpoint AR) (S m) *)
exact (interp (headCP cp)).
(* Goal: cartesianPowerAux (@COINCpoint AR) (S m) *)
exact (IHm (tailCP cp)).
Defined.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma interp_CPHdOK {m : nat} : forall (cp : cartesianPower positive (S m)) interp,
  interp_CP (headCPbis cp) interp = headCP (interp_CP cp interp).
Proof.
(* Goal: SS.elt *)
induction m.

(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  unfold interp_CP; unfold nat_rect; simpl; reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  induction m; unfold interp_CP; unfold nat_rect; simpl; reflexivity.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma interp_CPTlOK {m : nat} : forall (cp : cartesianPower positive (S (S m))) interp,
  interp_CP (tailCP cp) interp = tailCP (interp_CP cp interp).
Proof.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
induction m; unfold interp_CP; unfold nat_rect; simpl; reflexivity.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma interp_CPOK {m : nat} : forall (cp : cartesianPower positive (S m)) (interp: positive -> COINCpoint),
  CPToList (interp_CP cp interp) = map interp (CPToList cp).
Proof.
(* Goal: forall (cp : cartesianPower positive (S m)) (interp : forall _ : positive, @COINCpoint AR), @eq (list (@COINCpoint AR)) (@CPToList (@COINCpoint AR) (S m) (@interp_CP m cp interp)) (@map positive (@COINCpoint AR) interp (@CPToList positive (S m) cp)) *)
induction m; intros cp interp.

(* Goal: and (@eq positive (@headCP positive (S (S (@length positive l))) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e)) e) (@eq positive (@headCP positive (S (@length positive l)) (@tailCP positive (S (@length positive l)) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e))) e) *)
  simpl.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  reflexivity.

(* Goal: @eq (list (@COINCpoint AR)) (@CPToList (@COINCpoint AR) (S (S m)) (@interp_CP (S m) cp interp)) (@map positive (@COINCpoint AR) interp (@CPToList positive (S (S m)) cp)) *)
  induction m; try (clear IHm0).

(* Goal: and (@eq positive (@headCP positive (S (S (@length positive l))) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e)) e) (@eq positive (@headCP positive (S (@length positive l)) (@tailCP positive (S (@length positive l)) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e))) e) *)
    simpl.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
    reflexivity.

(* Goal: @eq (list (@COINCpoint AR)) (@CPToList (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S m)) cp interp)) (@map positive (@COINCpoint AR) interp (@CPToList positive (S (S (S m))) cp)) *)
    rewrite CPToListOK.
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (@n AR)) (@tailCP positive (S (@n AR)) cp') interp)) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
    rewrite <- interp_CPHdOK.
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
    rewrite <- interp_CPTlOK.
(* Goal: @eq (list (@COINCpoint AR)) (@cons (@COINCpoint AR) (@interp_CP O (@headCPbis positive (S (S m)) cp) interp) (@CPToList (@COINCpoint AR) (S (S m)) (@interp_CP (S m) (@tailCP positive (S m) cp) interp))) (@map positive (@COINCpoint AR) interp (@CPToList positive (S (S (S m))) cp)) *)
    rewrite IHm.
(* Goal: and (@eq positive (@headCP positive (S (S (@length positive l))) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e)) e) (@eq positive (@headCP positive (S (@length positive l)) (@tailCP positive (S (@length positive l)) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e))) e) *)
    simpl.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
    reflexivity.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Context {COP : Coinc_predicates AR}.

Definition ss_ok (ss : SS.t) (interp: positive -> COINCpoint) :=
  forall s, SS.mem s ss = true ->
  forall cp, memCP cp s = true ->
    app coinc (interp_CP cp interp).

Lemma consHdInterpOK : forall (cp : cartesianPower positive 1) (x : tST) interp,
  consHeadCP (interp_CP cp interp) (interp_CP x interp) = interp_CP (consHeadCP cp x) interp.
Proof.
(* Goal: forall (cp : cartesianPower positive (S O)) (x : @tST AR) (interp : forall _ : positive, @COINCpoint AR), @eq (cartesianPower (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR))))) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O cp interp) (@interp_CP (S (@n AR)) x interp)) (@interp_CP (S (S (@n AR))) (@consHeadCP (cartesianPower positive (S O)) (S (S (@n AR))) cp x) interp) *)
intros cp x interp.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
apply CP_ind; simpl; reflexivity.
Qed.

Lemma ss_ok_inter_ok1 : forall ss interp s1 s2 x (p : cartesianPower positive 1),
  ss_ok ss interp ->
  SS.In s1 ss ->
  pick_variety_aux (S.inter s1 s2) x = true ->
  S.mem p s1 = true ->
  app_1_n coinc (interp_CP p interp) (interp_CP x interp).
Proof.
(* Goal: forall (ss : SS.t) (interp : forall _ : positive, @COINCpoint AR) (s1 : S.t) (s2 : SS.elt) (x : @tST AR) (p : cartesianPower positive (S O)) (_ : ss_ok ss interp) (_ : SS.In s2 ss) (_ : @eq bool (pick_variety_aux (S.inter s1 s2) x) true) (_ : @eq bool (S.mem p s2) true), @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp) *)
intros ss interp s1 s2 x p HSSOK HIn HInter Hmem.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp) *)
apply app_app_1_n with (consHeadCP (interp_CP p interp) (interp_CP x interp)); try (simpl; reflexivity).
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp)) *)
assert (Hmemcp : memCPAux n x s1 = true) by (apply pick_variety_aux_memCPAux1 with s2; assumption).
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp)) *)
unfold ss_ok in HSSOK.
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp)) *)
rewrite consHdInterpOK.
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) (@consHeadCP (cartesianPower positive (S O)) (S (S (@n AR))) p x) interp) *)
apply SSWEqP.MP.Dec.F.mem_1 in HIn.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply HSSOK with s1; try assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply memCPConsHd; assumption.
Qed.

Lemma ss_ok_inter_ok2 : forall ss interp s1 s2 x (p : cartesianPower positive 1),
  ss_ok ss interp ->
  SS.In s2 ss ->
  pick_variety_aux (S.inter s1 s2) x = true ->
  S.mem p s2 = true ->
  app_1_n coinc (interp_CP p interp) (interp_CP x interp).
Proof.
(* Goal: forall (ss : SS.t) (interp : forall _ : positive, @COINCpoint AR) (s1 : S.t) (s2 : SS.elt) (x : @tST AR) (p : cartesianPower positive (S O)) (_ : ss_ok ss interp) (_ : SS.In s2 ss) (_ : @eq bool (pick_variety_aux (S.inter s1 s2) x) true) (_ : @eq bool (S.mem p s2) true), @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp) *)
intros ss interp s1 s2 x p HSSOK HIn HInter Hmem.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp) *)
apply app_app_1_n with (consHeadCP (interp_CP p interp) (interp_CP x interp)); try (simpl; reflexivity).
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp)) *)
assert (Hmemcp : memCPAux n x s2 = true) by (apply pick_variety_aux_memCPAux2 with s1; assumption).
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp)) *)
unfold ss_ok in HSSOK.
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@consHeadCP (cartesianPower (@COINCpoint AR) (S O)) (S (S (@n AR))) (@interp_CP O p interp) (@interp_CP (S (@n AR)) x interp)) *)
rewrite consHdInterpOK.
(* Goal: @app (cartesianPower (@COINCpoint AR) (S O)) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) (@consHeadCP (cartesianPower positive (S O)) (S (S (@n AR))) p x) interp) *)
apply SSWEqP.MP.Dec.F.mem_1 in HIn.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply HSSOK with s2; try assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply memCPConsHd; assumption.
Qed.

Lemma mca_pick_variety_aux_pca : forall m cp s1 s2 ss x interp,
  ss_ok ss interp ->
  SS.In s1 ss ->
  SS.In s2 ss ->
  memCPAux (S m) cp (S.union s1 s2) = true ->
  pick_variety_aux (S.inter s1 s2) x = true ->
  pred_conj_aux coinc (S (S m)) (interp_CP cp interp) (interp_CP x interp).
Proof.
(* Goal: forall (m : nat) (cp : cartesianPower positive (S (S (S m)))) (s1 s2 : SS.elt) (ss : SS.t) (x : @tST AR) (interp : forall _ : positive, @COINCpoint AR) (_ : ss_ok ss interp) (_ : SS.In s1 ss) (_ : SS.In s2 ss) (_ : @eq bool (memCPAux (S m) cp (S.union s1 s2)) true) (_ : @eq bool (pick_variety_aux (S.inter s1 s2) x) true), @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@interp_CP (S (S m)) cp interp) (@interp_CP (S (@n AR)) x interp) *)
induction m; intros cp s1 s2 ss x interp HSSOK HIn1 HIn2 Hmemcp Hhtspa.

(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S O)) (@interp_CP (S (S O)) cp interp) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
  unfold pred_conj_aux.
(* Goal: nat_rect (fun m : nat => forall _ : cartesianPower (@COINCpoint AR) (S m), Prop) (fun cp : cartesianPower (@COINCpoint AR) (S O) => @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) cp (@interp_CP (S (@n AR)) x interp)) (fun (m : nat) (IHm : forall _ : cartesianPower (@COINCpoint AR) (S m), Prop) (cp : cartesianPower (@COINCpoint AR) (S (S m))) => and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S m) cp) (@interp_CP (S (@n AR)) x interp)) (IHm (@tailCP (@COINCpoint AR) m cp))) (S (S O)) (@interp_CP (S (S O)) cp interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
  unfold nat_rect.
(* Goal: and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) (@pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) *)
  split.

(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    assert (HIn : InCP (headCP cp) cp) by (unfold InCP; simpl; auto).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S O)) (@interp_CP (S (S O)) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S O) (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp)) (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@tailCP (@COINCpoint AR) O (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp)) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
    assert (HElim : S.mem (headCP cp) (S.union s1 s2) = true) by (apply memCPAuxOK with 1 cp; assumption).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    rewrite SWP.FM.union_b in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    apply orb_true_iff in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    elim HElim; clear HElim; intro HElim.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply ss_ok_inter_ok1 with ss s1 s2; assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply ss_ok_inter_ok2 with ss s1 s2; assumption.

(* Goal: and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) (@pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) *)
    split.

(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S O) (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@tailCP (@COINCpoint AR) O (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
      assert (HIn : InCP (headCP (tailCP cp)) cp) by (unfold InCP; simpl; auto).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S O) (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@tailCP (@COINCpoint AR) O (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
      assert (HElim : S.mem (headCP (tailCP cp)) (S.union s1 s2) = true) by (apply memCPAuxOK with 1 cp; assumption).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
      rewrite SWP.FM.union_b in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
      apply orb_true_iff in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
      elim HElim; clear HElim; intro HElim.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
        apply ss_ok_inter_ok1 with ss s1 s2; assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
        apply ss_ok_inter_ok2 with ss s1 s2; assumption.

(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@tailCP (@COINCpoint AR) O (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
      assert (HIn : InCP (tailCP (tailCP cp)) cp) by (unfold InCP; simpl; auto).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@tailCP (@COINCpoint AR) O (@tailCP (@COINCpoint AR) (S O) (@interp_CP (S (S O)) cp interp))) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
      assert (HElim : S.mem (tailCP (tailCP cp)) (S.union s1 s2) = true) by (apply memCPAuxOK with 1 cp; assumption).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
      rewrite SWP.FM.union_b in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
      apply orb_true_iff in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
      elim HElim; clear HElim; intro HElim.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
        apply ss_ok_inter_ok1 with ss s1 s2; assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
        apply ss_ok_inter_ok2 with ss s1 s2; assumption.

(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
  rewrite pcaHdTl.
(* Goal: and (@app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) (@pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp)) *)
  split.

(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    assert (HIn : InCP (headCP cp) cp) by (unfold InCP; simpl; auto).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    assert (HElim : S.mem (headCP cp) (S.union s1 s2) = true) by (apply memCPAuxOK with (S (S m)) cp; assumption).
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    rewrite SWP.FM.union_b in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    apply orb_true_iff in HElim.
(* Goal: @app_1_n (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@headCP (@COINCpoint AR) (S (S (S m))) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: @pred_conj_aux (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (S (S m)) (@tailCP (@COINCpoint AR) (S (S m)) (@interp_CP (S (S (S m))) cp interp)) (@interp_CP (S (@n AR)) x interp) *)
    elim HElim; clear HElim; intro HElim.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply ss_ok_inter_ok1 with ss s1 s2; assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply ss_ok_inter_ok2 with ss s1 s2; assumption.

(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
    rewrite <- interp_CPTlOK.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply IHm with s1 s2 ss; try assumption.
(* Goal: @eq bool (memCPAux (S m) (@tailCP positive (S (S m)) cp) (S.union s1 s2)) true *)
    apply memCPAuxTlOK.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.
Qed.

Definition st_ok (st : STt) (interp: positive -> COINCpoint) :=
  forall t, STmem t st = true -> app wd (interp_CP t interp).

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Context {COT : Coinc_theory AR COP}.

Lemma identify_varieties_ok : forall ss st interp,
  ss_ok ss interp -> st_ok st interp ->
  ss_ok (identify_varieties ss st) interp.
Proof.
(* Goal: forall (ss : SS.t) (st : @STt AR) (interp : forall _ : positive, @COINCpoint AR) (_ : ss_ok ss interp) (_ : st_ok st interp), ss_ok (identify_varieties ss st) interp *)
intros ss st interp HSS HST.
apply (let P interp ss st newss :=
       ss_ok ss interp -> st_ok st interp -> ss_ok newss interp in
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
         identify_varieties_ind (P interp)); try assumption.

(* Goal: forall interp : forall _ : positive, @COINCpoint AR, st_ok (@STempty AR) interp *)
  intros.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  assumption.

(* Goal: forall (ss : SS.t) (st : @STt AR), let varieties := pick_varieties ss st in forall (s1 s2 : SS.elt) (_ : @eq (option (prod SS.elt SS.elt)) varieties (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt s1 s2))), let auxsetofsets := SS.remove s2 (SS.remove s1 ss) in let auxset := S.union s1 s2 in let newss := SS.add auxset auxsetofsets in forall (_ : forall (_ : ss_ok newss interp) (_ : st_ok st interp), ss_ok (identify_varieties newss st) interp) (_ : ss_ok ss interp) (_ : st_ok st interp), ss_ok (identify_varieties newss st) interp *)
  clear HSS; clear HST; clear ss; clear st.
(* Goal: forall (ss : SS.t) (st : @STt AR), let varieties := pick_varieties ss st in forall (s1 s2 : SS.elt) (_ : @eq (option (prod SS.elt SS.elt)) varieties (@Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt s1 s2))), let auxsetofsets := SS.remove s2 (SS.remove s1 ss) in let auxset := S.union s1 s2 in let newss := SS.add auxset auxsetofsets in forall (_ : forall (_ : ss_ok newss interp) (_ : st_ok st interp), ss_ok (identify_varieties newss st) interp) (_ : ss_ok ss interp) (_ : st_ok st interp), ss_ok (identify_varieties newss st) interp *)
  intros ss st varieties s1 s2 Hs1s2 auxsetofsets auxset newss H HSS HST.
(* Goal: ss_ok (identify_varieties newss st) interp *)
  assert (Hs1 := Hs1s2).
(* Goal: ss_ok (identify_varieties newss st) interp *)
  assert (Hs2 := Hs1s2).
(* Goal: ss_ok (identify_varieties newss st) interp *)
  apply pick_varieties_ok_1 in Hs1.
(* Goal: ss_ok (identify_varieties newss st) interp *)
  apply pick_varieties_ok_2 in Hs2.
(* Goal: ss_ok (identify_varieties newss st) interp *)
  apply SSWEqP.MP.Dec.F.remove_3 in Hs2.
(* Goal: ss_ok (identify_varieties newss st) interp *)
  apply H; try assumption; clear H.
(* Goal: ss_ok newss interp *)
  intros s Hmem cp Hmemcp.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
  unfold newss in Hmem; clear newss.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
  elim (SS.E.eq_dec auxset s); intro HEq.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    assert (HEq' : memCP cp auxset = memCP cp s) by (apply memCPProper; trivial).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    rewrite <- HEq in *; rewrite <- HEq' in *; clear HEq; clear HEq'; clear s.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    unfold varieties in Hs1s2; clear varieties.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    unfold pick_varieties in Hs1s2.
    case_eq (exists_witness
            (fun s : SS.elt =>
             match pick_varieties_aux s (SS.remove s ss) st with
             | Some _ => true
             | None => false
             end) ss); try (intro HEW; rewrite HEW in *; discriminate).
(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@Some SS.elt e)), @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    intros e1 HEW; rewrite HEW in *; clear HEW.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    unfold pick_varieties_aux in *.
    case_eq (exists_witness
            (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st)
            (SS.remove e1 ss)); try (intro HEW; rewrite HEW in *; discriminate).
(* Goal: forall (e : SS.elt) (_ : @eq (option SS.elt) (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)) (@Some SS.elt e)), @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    intros e2 HEW; rewrite HEW in *.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    injection Hs1s2; intros He2s2 He1s1.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    rewrite He2s2 in *; rewrite He1s1 in *; clear He2s2; clear He1s1; clear Hs1s2; clear e2; clear e1.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    case_eq (pick_variety (S.inter s1 s2) st).

(* Goal: forall _ : @eq (option SS.elt) (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some p => true | None => false end) ss) (@None SS.elt), SS.In s2 (SS.remove s1 ss) *)
      clear HEW; intro HEW.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: forall _ : @eq bool (pick_variety (S.inter s1 s2) st) false, @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      unfold pick_variety in HEW.
      apply STexists_mem_4 in HEW;
        try (intros x y Hxy; destruct Hxy as [Hxyfst Hxysnd]; rewrite Hxyfst; rewrite Hxysnd; reflexivity); try (apply proper_00).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: forall _ : @eq bool (pick_variety (S.inter s1 s2) st) false, @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      destruct HEW as [x [HmemST1 HmemST2]].
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: forall _ : @eq bool (pick_variety (S.inter s1 s2) st) false, @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      apply HST in HmemST1.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply coinc_n with (interp_CP x interp); try assumption.
(* Goal: @pred_conj (@COINCpoint AR) (S (S (@n AR))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) (@interp_CP (S (@n AR)) x interp) *)
(* Goal: forall _ : @eq bool (pick_variety (S.inter s1 s2) st) false, @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      unfold pred_conj.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply mca_pick_variety_aux_pca with s1 s2 ss; assumption.

(* Goal: forall _ : @eq bool (pick_variety (S.inter s1 s2) st) false, @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      intro HEW2; unfold exists_witness in *; apply SS.choose_spec1 in HEW.
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) *)
(* Goal: forall x : SS.elt, @eq bool (pick_variety (S.inter x1 x) y3) (pick_variety (S.inter y1 x) y3) *)
(* Goal: SS.Equal x2 y2 *)
(* Goal: eqopp match exists_witness (fun s2 : SS.elt => pick_variety (S.inter x1 s2) y3) x2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt x1 s2) | None => @None (prod SS.elt SS.elt) end match exists_witness (fun s2 : SS.elt => pick_variety (S.inter y1 s2) y3) y2 with | Some s2 => @Some (prod SS.elt SS.elt) (@pair SS.elt SS.elt y1 s2) | None => @None (prod SS.elt SS.elt) end *)
      apply SSWEqP.MP.Dec.F.filter_2 in HEW; try apply proper_1.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
      rewrite HEW2 in *; discriminate.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    rewrite SSWP.Dec.F.add_neq_b in Hmem; try assumption.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    apply HSS with s.
(* Goal: @eq bool (SS.mem s ss) true *)
(* Goal: @eq bool (memCP cp s) true *)
    unfold auxsetofsets in *.
(* Goal: @eq bool (SS.mem s ss) true *)
(* Goal: @eq bool (memCP cp s) true *)
    apply SSWEqP.MP.Dec.F.mem_2 in Hmem.
(* Goal: @eq bool (SS.mem s ss) true *)
(* Goal: @eq bool (memCP cp s) true *)
    do 2 (apply SSWEqP.MP.Dec.F.remove_3 in Hmem).
(* Goal: @eq bool (SS.mem s (identify_varieties ss st)) true *)
(* Goal: @eq bool (memCP cp s) true *)
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s : SS.elt => memCP cp s) *)
    apply SSWEqP.MP.Dec.F.mem_1.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.
Qed.

Lemma test_coinc_ok : forall ss st interp cp,
  ss_ok ss interp -> st_ok st interp ->
  test_coinc ss st cp = true ->
  app coinc (interp_CP cp interp).
Proof.
(* Goal: forall (ss : SS.t) (st : @STt AR) (interp : forall _ : positive, @COINCpoint AR) (cp : cartesianPower positive (S (S (S (@n AR))))) (_ : ss_ok ss interp) (_ : st_ok st interp) (_ : @eq bool (test_coinc ss st cp) true), @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
intros ss st interp cp HSS HST HTC.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
unfold test_coinc in *.
assert (HSS2 : ss_ok (identify_varieties ss st) interp)
  by (apply identify_varieties_ok; assumption).

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
unfold ss_ok in HSS2.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
apply SSWEqP.MP.Dec.F.exists_2 in HTC.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s : SS.elt => memCP cp s) *)
unfold SS.Exists in HTC.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s : SS.elt => memCP cp s) *)
destruct HTC as [s [HIn Hmem]].
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s : SS.elt => memCP cp s) *)
apply HSS2 with s.
(* Goal: @eq bool (SS.mem s (identify_varieties ss st)) true *)
(* Goal: @eq bool (memCP cp s) true *)
(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s : SS.elt => memCP cp s) *)
apply SSWEqP.MP.Dec.F.mem_1.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
assumption.

(* Goal: @Proper (forall _ : S.t, bool) (@respectful S.t bool S.Equal (@eq bool)) (fun s : SS.elt => memCP cp s) *)
intros x y Hxy.
(* Goal: @eq bool (memCP cp x) (memCP cp y) *)
apply memCPProper; trivial.
Qed.

Lemma ss_ok_empty : forall interp,
  ss_ok SS.empty interp.
Proof.
(* Goal: forall interp : forall _ : positive, @COINCpoint AR, ss_ok SS.empty interp *)
intros interp ss Hmem1 cp Hmem2.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
rewrite SSWEqP.MP.Dec.F.empty_b in Hmem1.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
discriminate.
Qed.

Lemma st_ok_empty : forall interp,
  st_ok STempty interp.
Proof.
(* Goal: forall interp : forall _ : positive, @COINCpoint AR, st_ok (@STempty AR) interp *)
intros.
(* Goal: st_ok (@STadd AR cp st) interp *)
unfold st_ok.
(* Goal: forall (t : @tST AR) (_ : @eq bool (@STmem AR t (@STempty AR)) true), @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
intros t Ht.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
rewrite STempty_b in Ht.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
discriminate.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Definition CPToSS {m:nat} (cp : cartesianPower positive m) : SS.elt.
Proof.
(* Goal: SS.elt *)
induction m.
(* Goal: SS.elt *)
(* Goal: SS.elt *)
exact S.empty.
(* Goal: SS.elt *)
induction m.
(* Goal: SS.elt *)
(* Goal: SS.elt *)
exact (S.add cp S.empty).
(* Goal: SS.elt *)
exact (S.add (headCP cp) (IHm (tailCP cp))).
Defined.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma CPToSSHdTl {m:nat} : forall (cp : cartesianPower positive (S (S m))),
  CPToSS cp = S.add (headCP cp) (CPToSS (tailCP cp)).
Proof. simpl; reflexivity. Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma memCPToSSOK {m : nat} : forall e (cp : cartesianPower positive (S m)),
  S.mem e (CPToSS cp) = true ->
  InCP e cp.
Proof.
(* Goal: forall (e : S.elt) (cp : cartesianPower positive (S m)) (_ : @eq bool (S.mem e (@CPToSS (S m) cp)) true), @InCP S.elt (S m) e cp *)
induction m; intros e cp Hmem.

(* Goal: @InCP S.elt (S O) e cp *)
(* Goal: @InCP S.elt (S (S m)) e cp *)
  unfold InCP.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  simpl in *.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  left.
(* Goal: @eq S.elt cp e *)
(* Goal: @InCP S.elt (S (S m)) e cp *)
  rewrite <- SWP.singleton_equal_add in Hmem.
(* Goal: @eq S.elt e (@headCP S.elt (S m) cp) *)
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  apply SWP.Dec.F.mem_2 in Hmem.
(* Goal: @eq S.elt cp e *)
(* Goal: @InCP S.elt (S (S m)) e cp *)
  apply SWP.Dec.F.singleton_1.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  assumption.

(* Goal: @InCP S.elt (S (S m)) e cp *)
  apply InCPOK.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  rewrite CPToSSHdTl in Hmem.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  rewrite SWP.Dec.F.add_b in Hmem.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  rewrite <- SWP.Dec.F.singleton_b in Hmem.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  apply orb_true_iff in Hmem.
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
  elim Hmem; clear Hmem; intro Hmem.

(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
    left.
(* Goal: @eq S.elt e (@headCP S.elt (S m) cp) *)
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
    apply SWP.Dec.F.mem_2 in Hmem.
(* Goal: @eq S.elt e (@headCP S.elt (S m) cp) *)
(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
    apply SWP.Dec.F.singleton_1 in Hmem.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    intuition.

(* Goal: or (@eq S.elt e (@headCP S.elt (S m) cp)) (@InCP S.elt (S m) e (@tailCP S.elt m cp)) *)
    right.
(* Goal: @InCP S.elt (S m) e (@tailCP S.elt m cp) *)
    apply IHm.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma CPToSSOKAux {m m' : nat} :
  forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S m'))) e s,
  S.Equal (CPToSS cp) s ->
  memCPAux m' cp' s = true ->
  InCP e cp' ->
  InCP e cp.
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S m'))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux m' cp' s) true) (_ : @InCP positive (S (S m')) e cp'), @InCP positive (S (S m)) e cp *)
induction m'.

(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S O))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux O cp' s) true) (_ : @InCP positive (S (S O)) e cp'), @InCP positive (S (S m)) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  induction m; intros cp cp' e s HEq Hmem HIn.

(* Goal: @InCP positive (S (S O)) e cp *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    unfold InCP in *.
(* Goal: @In positive e (@CPToList positive (S (S O)) cp) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    simpl in *.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    apply andb_true_iff in Hmem.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    destruct Hmem as [Hmem1 Hmem2].
    assert (HmemEq : S.mem (fst cp') (S.add (fst cp) (S.add (snd cp) S.empty)) = S.mem (fst cp') s)
      by (apply SWP.FM.mem_m; trivial); simpl in *;rewrite <- HmemEq in Hmem1; clear HmemEq.
    assert (HmemEq : S.mem (snd cp') (S.add (fst cp) (S.add (snd cp) S.empty)) = S.mem (snd cp') s)
      by (apply SWP.FM.mem_m; trivial); simpl in *;rewrite <- HmemEq in Hmem2; clear HmemEq; clear HEq.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    rewrite SWP.Dec.F.add_b in Hmem1.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    rewrite <- SWP.Dec.F.singleton_b in Hmem1.
    assert (HmemEq : S.mem (fst cp') (S.add (snd cp) S.empty) = S.mem (fst cp') (S.singleton (snd cp)))
      by (apply SWP.FM.mem_m; trivial; apply SWP.singleton_equal_add); simpl in *;rewrite HmemEq in Hmem1; clear HmemEq.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    rewrite SWP.Dec.F.add_b in Hmem2.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    rewrite <- SWP.Dec.F.singleton_b in Hmem2.
    assert (HmemEq : S.mem (snd cp') (S.add (snd cp) S.empty) = S.mem (snd cp') (S.singleton (snd cp)))
      by (apply SWP.FM.mem_m; trivial; apply SWP.singleton_equal_add); simpl in *;rewrite HmemEq in Hmem2; clear HmemEq.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    apply orb_true_iff in Hmem1.
(* Goal: or (@eq positive (@fst positive positive cp) e) (or (@eq positive (@snd positive positive cp) e) False) *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
    apply orb_true_iff in Hmem2.
(* Goal: @InCP positive (S (S m)) e cp *)
    elim HIn; clear HIn; intro HIn.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      subst.
      elim Hmem1; clear Hmem1; clear Hmem2; intro HEq; apply SWP.Dec.F.mem_2 in HEq;
      apply SWP.Dec.F.singleton_1 in HEq; auto.

(* Goal: @InCP positive (S (S m)) e cp *)
      elim HIn; clear HIn; intro HIn.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
        subst.
        elim Hmem2; clear Hmem1; clear Hmem2; intro HEq; apply SWP.Dec.F.mem_2 in HEq;
        apply SWP.Dec.F.singleton_1 in HEq; auto.

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
        intuition.

(* Goal: @InCP positive (S (S m)) e cp *)
    elim HIn; clear HIn; intro HIn.

      assert (HmemEq : memCPAux 0 cp' (CPToSS cp) = memCPAux 0 cp' s) by (apply memCPAuxProperOK; trivial);
(* Goal: cartesianPower (@COINCpoint AR) (S (S m)) *)
      rewrite <- HmemEq in Hmem; clear HmemEq; clear HEq; clear IHm.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
      subst.
(* Goal: @InCP positive (S (S m)) (@headCP positive (S (S m')) cp') cp *)
(* Goal: @InCP positive (S (S m)) e cp *)
      assert (HIn : InCP (headCP cp') cp') by (unfold InCP; simpl; auto).
(* Goal: @InCP positive (S (S (S m))) (@headCP positive (S O) cp') cp *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
      assert (H := memCPAuxOK 0 cp' (CPToSS cp) (headCP cp') Hmem HIn); clear HIn; clear Hmem; rename H into Hmem.
(* Goal: @InCP positive (S (S m)) (@headCP positive (S (S m')) cp') cp *)
(* Goal: @InCP positive (S (S m)) e cp *)
      apply memCPToSSOK.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
      assumption.

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
      unfold InCP in HIn.
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
      simpl in HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
      elim HIn; clear HIn; intro HIn.

        assert (HmemEq : memCPAux 0 cp' (CPToSS cp) = memCPAux 0 cp' s) by (apply memCPAuxProperOK; trivial);
(* Goal: cartesianPower (@COINCpoint AR) (S (S m)) *)
        rewrite <- HmemEq in Hmem; clear HmemEq; clear HEq; clear IHm.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
        subst.
(* Goal: @InCP positive (S (S (S m))) (@snd positive positive cp') cp *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
        assert (HIn : InCP (tailCP cp') cp') by (unfold InCP; simpl; auto).
(* Goal: @InCP positive (S (S (S m))) (@snd positive positive cp') cp *)
(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
        assert (H := memCPAuxOK 0 cp' (CPToSS cp) (tailCP cp') Hmem HIn); clear HIn; clear Hmem; rename H into Hmem.
(* Goal: @InCP positive (S (S m)) (@headCP positive (S (S m')) cp') cp *)
(* Goal: @InCP positive (S (S m)) e cp *)
        apply memCPToSSOK.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
        assumption.

(* Goal: @InCP positive (S (S (S m))) e cp *)
(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
        intuition.

(* Goal: forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S (S m')))) (e : positive) (s : S.t) (_ : S.Equal (@CPToSS (S (S m)) cp) s) (_ : @eq bool (memCPAux (S m') cp' s) true) (_ : @InCP positive (S (S (S m'))) e cp'), @InCP positive (S (S m)) e cp *)
  intros cp cp' e s HEq Hmem HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
  apply InCPOK in HIn.
(* Goal: @InCP positive (S (S m)) e cp *)
  elim HIn; clear HIn; intro HIn.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
    subst.
    assert (HmemEq : memCPAux (S m') cp' (CPToSS cp) = memCPAux (S m') cp' s) by (apply memCPAuxProperOK; trivial);
    rewrite <- HmemEq in Hmem; clear HmemEq; clear HEq; clear IHm'.
(* Goal: @InCP positive (S (S m)) (@headCP positive (S (S m')) cp') cp *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assert (HIn : InCP (headCP cp') cp') by (unfold InCP; simpl; auto).
(* Goal: @InCP positive (S (S m)) (@headCP positive (S (S m')) cp') cp *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assert (H := memCPAuxOK (S m') cp' (CPToSS cp) (headCP cp') Hmem HIn); clear HIn; clear Hmem; rename H into Hmem.
(* Goal: @InCP positive (S (S m)) (@headCP positive (S (S m')) cp') cp *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply memCPToSSOK.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply IHm' with (tailCP cp') s; try assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply memCPAuxTlOK; assumption.
Qed.

Lemma CPToSSOK : forall (cp cp' : cartesianPower positive (S (S (S n)))) s,
  S.Equal (CPToSS cp) s ->
  memCP cp' s = true ->
  incl (CPToList cp') (CPToList cp).
Proof.
(* Goal: forall (cp cp' : cartesianPower positive (S (S (S (@n AR))))) (s : S.t) (_ : S.Equal (@CPToSS (S (S (S (@n AR)))) cp) s) (_ : @eq bool (memCP cp' s) true), @incl positive (@CPToList positive (S (S (S (@n AR)))) cp') (@CPToList positive (S (S (S (@n AR)))) cp) *)
unfold incl.
(* Goal: forall (cp cp' : cartesianPower positive (S (S (S (@n AR))))) (s : S.t) (_ : S.Equal (@CPToSS (S (S (S (@n AR)))) cp) s) (_ : @eq bool (memCP cp' s) true) (a : positive) (_ : @In positive a (@CPToList positive (S (S (S (@n AR)))) cp')), @In positive a (@CPToList positive (S (S (S (@n AR)))) cp) *)
intros cp cp' s HEq Hmem e HIn.
(* Goal: @In positive e (@CPToList positive (S (S (S (@n AR)))) cp) *)
assert (H := CPToSSOKAux cp cp' e s HEq Hmem).
(* Goal: @In positive e (@CPToList positive (S (S (S (@n AR)))) cp) *)
unfold InCP in H.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply H; assumption.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma CoappDupPerm {m : nat} :
  forall (cp : cartesianPower positive m),
  ~ List.NoDup (CPToList cp) ->
  exists e, exists l, Permutation.Permutation (CPToList (ListToCP (e :: e :: l) e)) (CPToList cp).
Proof.
(* Goal: forall (cp : cartesianPower positive m) (_ : not (@NoDup positive (@CPToList positive m cp))), @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
intros cp HDup.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
apply NotNoDupDup in HDup; try apply Pos.eq_dec.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
destruct HDup as [e [l1 [l2 [HEq HIn]]]].
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
apply in_split in HIn.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
destruct HIn as [l3 [l4 HEq']].
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
assert (HPerm := Permutation.Permutation_middle l1 l2 e).
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
rewrite <- HEq in HPerm; clear HEq.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
rewrite HEq' in HPerm; clear HEq'; clear l1; clear l2; rename l3 into l1; rename l4 into l2.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
assert (HPerm' := Permutation.Permutation_middle l1 l2 e).
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
apply (Permutation.perm_skip e) in HPerm'.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
assert (HPerm'' := Permutation.perm_trans HPerm' HPerm); clear HPerm; clear HPerm'; rename HPerm'' into HPerm.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun l : list positive => @Permutation.Permutation positive (@CPToList positive (@length positive (@cons positive e (@cons positive e l))) (@ListToCP positive (@cons positive e (@cons positive e l)) e)) (@CPToList positive m cp))) *)
rewrite <- CPLOK with (e :: e :: l1 ++ l2) e in HPerm.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
exists e; exists (l1 ++ l2); assumption.
Qed.

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma CoappDupAux {m : nat} :
  forall (cp : cartesianPower positive (S (S (S m)))),
  ~ List.NoDup (CPToList cp) ->
  exists e, exists (l : list positive), exists m', exists (cp' : cartesianPower positive (S (S (S m')))),
  Permutation.Permutation (CPToList cp') (CPToList cp) /\ headCP cp' = e /\ headCP (tailCP cp') = e.
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S (S m)))) (_ : not (@NoDup positive (@CPToList positive (S (S (S m))) cp))), @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
intros cp H.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
apply CoappDupPerm in H.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
destruct H as [e[l HPerm]].
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
assert (Hl := Permutation.Permutation_length HPerm).
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
rewrite CPLOK in Hl.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
rewrite <- lengthOfCPToList in Hl.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
induction l; try (simpl in Hl; discriminate); clear IHl.
(* Goal: @ex positive (fun e : positive => @ex (list positive) (fun _ : list positive => @ex nat (fun m' : nat => @ex (cartesianPower positive (S (S (S m')))) (fun cp' : cartesianPower positive (S (S (S m'))) => and (@Permutation.Permutation positive (@CPToList positive (S (S (S m'))) cp') (@CPToList positive (S (S (S m))) cp)) (and (@eq positive (@headCP positive (S (S m')) cp') e) (@eq positive (@headCP positive (S m') (@tailCP positive (S m') cp')) e)))))) *)
exists e; exists (a :: l); exists (length l); exists (ListToCP (e :: e :: a :: l) e).
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
split; try assumption.
(* Goal: and (@eq positive (@headCP positive (S (S (@length positive l))) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e)) e) (@eq positive (@headCP positive (S (@length positive l)) (@tailCP positive (S (@length positive l)) (@ListToCP positive (@cons positive e (@cons positive e (@cons positive a l))) e))) e) *)
simpl.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
split; reflexivity.
Qed.

Lemma CoappDup : forall cp interp,
  ~ List.NoDup (CPToList cp) ->
  app coinc (interp_CP cp interp).
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S (S (@n AR))))) (interp : forall _ : positive, @COINCpoint AR) (_ : not (@NoDup positive (@CPToList positive (S (S (S (@n AR)))) cp))), @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
intros cp interp H.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
apply CoappDupAux in H.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
destruct H as [e [l [m' [cp' [HPerm [Hfst Hsnd]]]]]].
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
assert (Hmn := Permutation.Permutation_length HPerm).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
apply Permutation.Permutation_map with positive COINCpoint interp (CPToList cp') (CPToList cp) in HPerm.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
do 2 (rewrite <- interp_CPOK in HPerm).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
do 2 (rewrite <- lengthOfCPToList in Hmn).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
do 3 (apply eq_add_S in Hmn).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
subst.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
apply PermCoincOK with (interp_CP cp' interp); try assumption; clear HPerm.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
apply app_2_n_app with (interp (headCP cp')) (interp (headCP (tailCP cp'))) (interp_CP (tailCP (tailCP cp')) interp).

(* Goal: @app_2_n (@COINCpoint AR) (S (@n AR)) (@coinc AR COP) (interp (@headCP positive (S (S (@n AR))) cp')) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (S (@n AR))) (@interp_CP (S (S (@n AR))) cp' interp)) (interp (@headCP positive (S (S (@n AR))) cp')) *)
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  rewrite Hsnd.
(* Goal: @app_2_n (@COINCpoint AR) (S (@n AR)) (@coinc AR COP) (interp (@headCP positive (S (S (@n AR))) cp')) (interp (@headCP positive (S (S (@n AR))) cp')) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (S (@n AR))) (@interp_CP (S (S (@n AR))) cp' interp)) (interp (@headCP positive (S (S (@n AR))) cp')) *)
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  apply coinc_bd.

(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (@n AR)) (@tailCP positive (S (@n AR)) cp') interp)) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  rewrite <- interp_CPHdOK.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  reflexivity.

(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  rewrite <- interp_CPTlOK.
(* Goal: @eq (@COINCpoint AR) (@headCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (@n AR)) (@tailCP positive (S (@n AR)) cp') interp)) (interp (@headCP positive (S (@n AR)) (@tailCP positive (S (@n AR)) cp'))) *)
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  rewrite <- interp_CPHdOK.
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  reflexivity.

(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@tailCP (@COINCpoint AR) (@n AR) (@tailCP (@COINCpoint AR) (S (@n AR)) (@interp_CP (S (S (@n AR))) cp' interp))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  do 2 (rewrite <- interp_CPTlOK).
(* Goal: @eq (cartesianPower (@COINCpoint AR) (S (@n AR))) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) (@interp_CP (@n AR) (@tailCP positive (@n AR) (@tailCP positive (S (@n AR)) cp')) interp) *)
  reflexivity.
Qed.

Lemma collect_coincs :
forall cp ss interp,
  app coinc (interp_CP cp interp) ->
  ss_ok ss interp -> ss_ok (SS.add (CPToSS cp) ss) interp.
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S (S (@n AR))))) (ss : SS.t) (interp : forall _ : positive, @COINCpoint AR) (_ : @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp)) (_ : ss_ok ss interp), ss_ok (SS.add (@CPToSS (S (S (S (@n AR)))) cp) ss) interp *)
intros cp ss interp HCoapp HSS.
(* Goal: ss_ok (SS.add (@CPToSS (S (S (S (@n AR)))) cp) ss) interp *)
unfold ss_ok.
(* Goal: forall (s : SS.elt) (_ : @eq bool (SS.mem s (SS.add (@CPToSS (S (S (S (@n AR)))) cp) ss)) true) (cp : cartesianPower positive (S (S (S (@n AR))))) (_ : @eq bool (memCP cp s) true), @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp interp) *)
intros s Hs.
(* Goal: forall (t : @tST AR) (_ : @eq bool (@STmem AR t (@STadd AR cp st)) true), @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
intros cp' Hmem.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
apply SSWEqP.MP.Dec.F.mem_2 in Hs.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
apply SSWEqP.MP.Dec.F.add_iff in Hs.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
elim Hs; clear Hs; intro Hs.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
  assert (HDup := NoDup_dec (CPToList cp') Pos.eq_dec).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
  elim HDup; clear HDup; intro HDup.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
    assert (Hincl := CPToSSOK cp cp' s Hs Hmem).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
    assert (Hlength : length (CPToList cp') = length (CPToList cp)) by (do 2 (rewrite <- lengthOfCPToList); reflexivity).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
    assert (HPerm := NoDupOK (CPToList cp') (CPToList cp) Hincl Hlength HDup).
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
    apply Permutation.Permutation_map with positive COINCpoint interp (CPToList cp') (CPToList cp) in HPerm.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
    do 2 (rewrite <- interp_CPOK in HPerm); clear HDup; clear Hincl; clear Hlength.
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
    apply Permutation.Permutation_sym in HPerm.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply PermCoincOK with (interp_CP cp interp); assumption.

(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
    apply CoappDup; assumption.

(* Goal: @app (@COINCpoint AR) (S (S (S (@n AR)))) (@coinc AR COP) (@interp_CP (S (S (@n AR))) cp' interp) *)
  unfold ss_ok in HSS.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply HSS with s; try assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
  apply SSWEqP.MP.Dec.F.mem_1; assumption.
Qed.

Lemma collect_wds :
  forall cp st interp,
  app wd (interp_CP cp interp) ->
  st_ok st interp -> st_ok (STadd cp st) interp.
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S (@n AR)))) (st : @STt AR) (interp : forall _ : positive, @COINCpoint AR) (_ : @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp interp)) (_ : st_ok st interp), st_ok (@STadd AR cp st) interp *)
intros cp st interp HWd HST.
(* Goal: st_ok (@STadd AR cp st) interp *)
unfold st_ok.
(* Goal: forall (t : @tST AR) (_ : @eq bool (@STmem AR t (@STadd AR cp st)) true), @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) t interp) *)
intros cp' Hmem.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp' interp) *)
apply STadd_iff in Hmem.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp' interp) *)
elim Hmem; clear Hmem; intro Hmem; [|apply HST; apply Hmem].
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp' interp) *)
assert (Hcp := sets.PosSort.Permuted_sort (CPToList cp)).
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp' interp) *)
assert (Hcp' := sets.PosSort.Permuted_sort (CPToList cp')).
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp' interp) *)
apply eqListOK in Hmem.
(* Goal: @app (@COINCpoint AR) (S (S (@n AR))) (@wd AR COP) (@interp_CP (S (@n AR)) cp' interp) *)
rewrite Hmem in Hcp.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply PermWdOK with (interp_CP cp interp); try assumption.
(* Goal: @Permutation.Permutation (@COINCpoint AR) (@CPToList (@COINCpoint AR) (S (S (@n AR))) (@interp_CP (S (@n AR)) cp interp)) (@CPToList (@COINCpoint AR) (S (S (@n AR))) (@interp_CP (S (@n AR)) cp' interp)) *)
do 2 (rewrite interp_CPOK).
(* Goal: @Permutation.Permutation (@COINCpoint AR) (@map positive (@COINCpoint AR) interp (@CPToList positive (S (S (@n AR))) cp)) (@map positive (@COINCpoint AR) interp (@CPToList positive (S (S (@n AR))) cp')) *)
apply Permutation.Permutation_map.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
transitivity (PosSort.sort (CPToList cp')); try assumption.
(* Goal: @eq bool (S.mem (@headCP positive (S (S m')) cp') (@CPToSS (S (S m)) cp)) true *)
(* Goal: @InCP positive (S (S m)) e cp *)
apply Permutation.Permutation_sym; assumption.
Qed.

Definition list_assoc_inv :=
  (fix list_assoc_inv_rec (A:Type) (B:Set)
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
                          (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
                          (lst : list (prodT A B)) {struct lst} : B -> A -> A :=
  fun (key:B) (default:A) =>
    match lst with
      | nil => default
      | cons (pairT v e) l =>
        match eq_dec e key with
          | left _ => v
          | right _ => list_assoc_inv_rec A B eq_dec l key default
        end
    end).

(* Goal: eqList (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t1)) (@CPToList positive (S (S (@n AR))) (@OCP (@n AR) t2)) *)
(* Goal: @InCP positive (S (S (@n AR))) p (@OCP (@n AR) t2) *)
Lemma positive_dec : forall (p1 p2:positive), {p1=p2}+{~p1=p2}.
Proof.
(* Goal: forall p1 p2 : positive, sumbool (@eq positive p1 p2) (not (@eq positive p1 p2)) *)
decide equality.
Defined.

Definition interp (lvar : list (COINCpoint * positive)) (Default : COINCpoint) : positive -> COINCpoint := 
  fun p => list_assoc_inv COINCpoint positive positive_dec lvar p Default.

End Coinc_refl.

Ltac add_to_distinct_list x xs :=
  match xs with
    | nil     => constr:(x::xs)
    | x::_    => fail 1
    | ?y::?ys => let zs := add_to_distinct_list x ys in constr:(y::zs)
  end.

Ltac collect_points_list Tpoint xs :=
  match goal with
    | N : Tpoint |- _ => let ys := add_to_distinct_list N xs in
                           collect_points_list Tpoint ys
    | _               => xs
  end.

Ltac collect_points Tpoint := collect_points_list Tpoint (@nil Tpoint).

Ltac number_aux Tpoint lvar cpt :=
  match constr:(lvar) with
    | nil          => constr:(@nil (prodT Tpoint positive))
    | cons ?H ?T => let scpt := eval vm_compute in (Pos.succ cpt) in
                    let lvar2 := number_aux Tpoint T scpt in
                      constr:(cons (@pairT  Tpoint positive H cpt) lvar2)
  end.

Ltac number Tpoint lvar := number_aux Tpoint lvar (1%positive).

Ltac build_numbered_points_list Tpoint := let lvar := collect_points Tpoint in number Tpoint lvar.

Ltac List_assoc Tpoint elt lst :=
  match constr:(lst) with
    | nil => fail
    | (cons (@pairT Tpoint positive ?X1 ?X2) ?X3) =>
      match constr:(elt = X1) with
        | (?X1 = ?X1) => constr:(X2)
        | _ => List_assoc Tpoint elt X3
      end
  end.

Definition Tagged P : Prop := P.

Lemma PropToTagged : forall P : Prop, P -> Tagged P.
Proof. trivial. Qed.