(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import ZArith NArith Nnat Ndec Ndigits.
From IntMap Require Import Map.
From IntMap Require Import Allmaps.
Require Import Relation_Definitions.
Require Import List.

Require Import misc.

Section my_MapFold.

Variable M : Set.
Variable neutral : M.
Variable op : M -> M -> M.
Variable R : relation M.

Definition F (A : Set) (f : ad -> A -> M) (r : ad * A) 
  (m : M) := let (a, y) := r in op (f a y) m.

Hypothesis eq_R : equiv _ R.
Hypothesis op_assoc : forall a b c : M, R (op (op a b) c) (op a (op b c)).
Hypothesis op_neutral_left : forall a : M, R (op neutral a) a.
Hypothesis op_neutral_right : forall a : M, R (op a neutral) a.
Hypothesis
  op_eq : forall a b a1 b1 : M, R a a1 -> R b b1 -> R (op a b) (op a1 b1).

Lemma op_eq_2 : forall a b b1 : M, R b b1 -> R (op a b) (op a b1).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  apply op_eq.  apply (proj1 eq_R).  assumption.
Qed.


Lemma my_fold_right_aapp :
 forall (A : Set) (f : ad -> A -> M) (l l' : alist A),
 R (fold_right (F A f) neutral (aapp _ l l'))
   (op (fold_right (F A f) neutral l) (fold_right (F A f) neutral l')).
Proof.
(* Goal: forall (A B : Set) (f : forall (_ : ad) (_ : A), Map B) (l : alist A) (_ : f_OK A B f) (_ : no_dup_alist A l) (a : ad) (y : B), iff (@eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l) a) (@Some B y)) (@ex ad (fun a1 : ad => @ex A (fun y1 : A => and (@In (prod ad A) (@pair ad A a1 y1) l) (@eq (option B) (MapGet B (f a1 y1) a) (@Some B y))))) *)
  simple induction l.  unfold F in |- *.  simpl in |- *.  intro.  apply (proj2 (proj2 eq_R)).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  apply op_neutral_left.  intros r l0 H1 l'.  elim r.  intros a y.  simpl in |- *.
  apply
   (proj1 (proj2 eq_R))
    with
      (y := op (f a y)
              (op (fold_right (F A f) neutral l0)
                 (fold_right (F A f) neutral l'))).
(* Goal: R (op (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0)) (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) (@fold_right M (prod ad A) (F A f) neutral (aapp A (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0) (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) *)
  apply op_eq_2.  apply H1.  apply (proj2 (proj2 eq_R)).  apply op_assoc.
Qed.


Lemma myMapFold_as_fold_1 :
 forall (A : Set) (f : ad -> A -> M) (m : Map A) (pf : ad -> ad),
 R (MapFold1 _ M neutral op f pf m)
   (fold_right (fun (r : ad * A) (m : M) => let (a, y) := r in op (f a y) m)
      neutral
      (MapFold1 _ (alist A) (anil A) (aapp A)
         (fun (a : ad) (y : A) => acons _ (a, y) (anil _)) pf m)).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  trivial.  intros.  simpl in |- *.  apply (proj1 eq_R).  intros.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simpl in |- *.  apply (proj2 (proj2 eq_R)).  apply op_neutral_right.  intros.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simpl in |- *.  fold (F A f) in |- *.  fold (F A f) in H.  fold (F A f) in H0.
  apply
   (proj1 (proj2 eq_R))
    with
      (y := op
              (fold_right (F A f) neutral
                 (MapFold1 A (alist A) (anil A) (aapp A)
                    (fun (a : ad) (y : A) => acons A (a, y) (anil A))
                    (fun a0 : ad => pf (Ndouble a0)) m0))
              (fold_right (F A f) neutral
                 (MapFold1 A (alist A) (anil A) (aapp A)
                    (fun (a : ad) (y : A) => acons A (a, y) (anil A))
                    (fun a0 : ad => pf (Ndouble_plus_one a0)) m1))).
(* Goal: R (op (MapFold1 A M neutral op f (fun a0 : ad => pf (N.double a0)) m0) (MapFold1 A M neutral op f (fun a0 : ad => pf (N.succ_double a0)) m1)) (op (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0)) (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) *)
(* Goal: R (op (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0)) (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) (@fold_right M (prod ad A) (F A f) neutral (aapp A (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0) (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) *)
  apply op_eq.  apply H.  apply H0.  apply (proj2 (proj2 eq_R)).
(* Goal: R (@fold_right M (prod ad A) (F A f) neutral (aapp A (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0) (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) (op (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.double a0)) m0)) (@fold_right M (prod ad A) (F A f) neutral (MapFold1 A (alist A) (anil A) (aapp A) (fun (a : ad) (y : A) => acons A (@pair ad A a y) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1))) *)
  apply my_fold_right_aapp.
Qed.

Lemma myMapFold_as_fold :
 forall (A : Set) (f : ad -> A -> M) (m : Map A),
 R (MapFold _ M neutral op f m)
   (fold_right (fun (r : ad * A) (m : M) => let (a, y) := r in op (f a y) m)
      neutral (alist_of_Map _ m)).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
intros.  exact (myMapFold_as_fold_1 A f m (fun a0 : ad => a0)).
Qed.

End my_MapFold.

(* Next we show the assumptions in the previous section are satisfied if M is
   a set of maps, neutral is the empty map, op is MapMerge and R is eqmap *)

(* eqmap is an equivalence relation *)
Lemma eqmap_equiv : forall A : Set, equiv _ (eqmap A).
Proof.
(* Goal: forall A : Set, equiv (Map A) (eqmap A) *)
  unfold equiv, eqmap in |- *.  unfold reflexive, symmetric, transitive in |- *.  split.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold eqm in |- *.  reflexivity.  split.  unfold eqm in |- *.  intros.  rewrite H.  apply H0.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold eqm in |- *.  intros.  rewrite (H a).  reflexivity.
Qed.

(* MapMerge is associative *)
Lemma MapMerge_assoc :
 forall (A : Set) (a b c : Map A),
 eqmap _ (MapMerge _ (MapMerge _ a b) c) (MapMerge _ a (MapMerge _ b c)).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold eqmap in |- *.  unfold eqm in |- *.  intros.  rewrite (MapMerge_semantics A (MapMerge A a b) c a0).
(* Goal: @eq (option A) match MapGet A c a0 with | Some y' => @Some A y' | None => MapGet A (MapMerge A a b) a0 end (MapGet A (MapMerge A a (MapMerge A b c)) a0) *)
  rewrite (MapMerge_semantics A a (MapMerge A b c) a0).  rewrite (MapMerge_semantics A a b a0).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite (MapMerge_semantics A b c a0).  elim (MapGet A c a0).  reflexivity.
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  reflexivity.
Qed.

(* M0 is the left identity *)
Lemma MapMerge_neutral_left :
 forall (A : Set) (m : Map A), eqmap _ (MapMerge _ (M0 A) m) m.
Proof.
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  unfold eqmap, eqm, MapMerge in |- *.  reflexivity.
Qed.

(* M0 is the right identity *)
Lemma MapMerge_neutral_right :
 forall (A : Set) (m : Map A), eqmap _ (MapMerge _ m (M0 _)) m.
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold eqmap in |- *.  unfold eqm in |- *.  unfold MapMerge in |- *.  intros.  elim m.  reflexivity.
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  reflexivity.  reflexivity.
Qed.

(* MapMerge preserves the eqmap relation *)
Lemma MapMerge_eq :
 forall (A : Set) (a a1 b b1 : Map A),
 eqmap _ a a1 -> eqmap _ b b1 -> eqmap _ (MapMerge _ a b) (MapMerge _ a1 b1).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold eqmap in |- *.  unfold eqm in |- *.  intros.  rewrite (MapMerge_semantics A a b a0).
(* Goal: @eq (option A) match MapGet A b a0 with | Some y' => @Some A y' | None => MapGet A a a0 end (MapGet A (MapMerge A a1 b1) a0) *)
  rewrite (MapMerge_semantics A a1 b1 a0).  rewrite (H a0).  rewrite (H0 a0).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  reflexivity.
Qed.

(* The net result : a semantics for MapCollect in terms of lists *)
Lemma myMapFold_as_fold_2 :
 forall (A B : Set) (f : ad -> A -> Map B) (m : Map A),
 eqmap _ (MapFold _ (Map B) (M0 _) (MapMerge _) f m)
   (fold_right
      (fun (r : ad * A) (m : Map B) =>
       let (a, y) := r in MapMerge _ (f a y) m) (M0 _) 
      (alist_of_Map _ m)).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  apply myMapFold_as_fold.  exact (eqmap_equiv B).  intros.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply MapMerge_assoc.  intros.  apply MapMerge_neutral_left.  intros.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply MapMerge_neutral_right.  intros.  apply MapMerge_eq.  assumption.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.
Qed.

Lemma my_alist_of_map_lemma_1 :
 forall (A : Set) (m : Map A) (a : ad) (y : A),
 MapGet _ m a = Some y -> In (a, y) (alist_of_Map _ m).
Proof.
(* Goal: forall (A : Set) (m : Map A) (a : ad) (y : A) (_ : @eq (option A) (MapGet A m a) (@Some A y)), @In (prod ad A) (@pair ad A a y) (alist_of_Map A m) *)
  intros A m a y.  rewrite (alist_of_Map_semantics _ m a).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  generalize (alist_of_Map A m).  simple induction a0.  simpl in |- *.  intro; discriminate.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simpl in |- *.  intro a1.  elim a1.  intros a2 b l H H0.  elim (sumbool_of_bool (Neqb a2 a)).
(* Goal: forall _ : @eq ad (pf a) a1, or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp a1) m') false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall _ : @In ad a1 l, or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp a1) m') false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m0 m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m0) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m m0) m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m m0)) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a))) *)
  intro H1.  left.  rewrite H1 in H0.  injection H0; intro H2.  rewrite H2.
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite (Neqb_complete _ _ H1).  reflexivity.  intro H1.  rewrite H1 in H0.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  right.  apply H.  assumption.
Qed.

Lemma my_alist_of_map_lemma_2 :
 forall (A : Set) (m : Map A) (pf fp : ad -> ad),
 (forall a : ad, fp (pf a) = a) ->
 forall (a : ad) (y : A),
 In (a, y)
   (MapFold1 _ _ (anil _) (aapp _)
      (fun (a : ad) (y : A) => acons _ (a, y) (anil _)) pf m) ->
 MapGet _ m (fp a) = Some y /\ pf (fp a) = a.
Proof.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simple induction m.  simpl in |- *.  tauto.  simpl in |- *.  intros a a0 pf fp H a1 y H0.  elim H0.  intro H1.
(* Goal: and (@eq bool (in_dom A (fp (pf a)) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp (pf a)) m') false) (@eq ad (pf (fp (pf a))) (pf a))) *)
(* Goal: forall _ : @In ad a1 l, or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp a1) m') false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m0 m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m0) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m m0) m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m m0)) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a))) *)
  injection H1; intros H2 H3.  rewrite <- H3.  rewrite (H a).  rewrite (Neqb_correct a).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite H2.  split; reflexivity.  tauto.  intros m0 H m1 H0 pf fp H1 a y H2.  simpl in H2.  unfold aapp in H2.
  elim
   (in_app_or
      (MapFold1 A (list (ad * A)) (anil A) (app (A:=ad * A))
         (fun (a0 : ad) (y0 : A) => acons A (a0, y0) (anil A))
         (fun a0 : ad => pf (Ndouble a0)) m0)
      (MapFold1 A (list (ad * A)) (anil A) (app (A:=ad * A))
         (fun (a0 : ad) (y0 : A) => acons A (a0, y0) (anil A))
         (fun a0 : ad => pf (Ndouble_plus_one a0)) m1) 
      (a, y) H2).
(* Goal: forall _ : and (@eq bool (in_dom A (fp a1) (MapRemove A (M2 A m0 m1) a)) true) (@eq ad (pf (fp a1)) a1), or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a1) (M1 B a a0)) false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m) false) (@eq ad (pf (fp a)) a)))) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m2) false) (@eq ad (pf (fp a)) a)))) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2))), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m m2)) false) (@eq ad (pf (fp a)) a))) *)
  intro H3.  fold (aapp A) in H3.  rewrite (MapGet_M2_bit_0_if A m0 m1 (fp a)).
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble a))) = a).
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intro H4.  elim
   (H (fun a0 : ad => pf (Ndouble a0)) (fun a0 : ad => Ndiv2 (fp a0)) H4
      a y H3).
(* Goal: forall (_ : @eq (option A) (MapGet A m1 (N.div2 (fp a))) (@Some A y)) (_ : @eq ad (pf (N.succ_double (N.div2 (fp a)))) a), and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intros H5 H6.  elim (sumbool_of_bool (Nbit0 (fp a))).  intro H7.
(* Goal: and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a y) (MapFold1 A (list (prod ad A)) (anil A) (@app (prod ad A)) (fun (a0 : ad) (y0 : A) => acons A (@pair ad A a0 y0) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1), and (@eq (option A) (MapGet A (M2 A m0 m1) (fp a)) (@Some A y)) (@eq ad (pf (fp a)) a) *)
  cut (Neqb (Ndouble (Ndiv2 (fp a))) (fp a) = false).  intro H8.
(* Goal: and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: @eq bool (N.eqb (N.double (N.div2 (fp a))) (fp a)) false *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a y) (MapFold1 A (list (prod ad A)) (anil A) (@app (prod ad A)) (fun (a0 : ad) (y0 : A) => acons A (@pair ad A a0 y0) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1), and (@eq (option A) (MapGet A (M2 A m0 m1) (fp a)) (@Some A y)) (@eq ad (pf (fp a)) a) *)
  cut (fp (pf (Ndouble (Ndiv2 (fp a)))) = fp a).  rewrite (H1 (Ndouble (Ndiv2 (fp a)))).
(* Goal: forall _ : @eq ad (N.double (N.div2 (fp a))) (fp a), and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: @eq ad (fp (pf (N.double (N.div2 (fp a))))) (fp a) *)
(* Goal: @eq bool (N.eqb (N.double (N.div2 (fp a))) (fp a)) false *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a y) (MapFold1 A (list (prod ad A)) (anil A) (@app (prod ad A)) (fun (a0 : ad) (y0 : A) => acons A (@pair ad A a0 y0) (anil A)) (fun a0 : ad => pf (N.succ_double a0)) m1), and (@eq (option A) (MapGet A (M2 A m0 m1) (fp a)) (@Some A y)) (@eq ad (pf (fp a)) a) *)
  intro H9.  rewrite H9 in H8.  rewrite (Neqb_correct (fp a)) in H8.  discriminate.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite H6.  reflexivity.  apply Nodd_not_double.  assumption.  intro H7.
(* Goal: @eq (option B) match MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0 with | Some y' => @Some B y' | None => MapGet B (f a y) a0 end (@Some B y0) *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a1 y1) l0, @eq (option B) (MapGet B (MapMerge B (f a y) (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l0)) a0) (@Some B y0) *)
(* Goal: no_dup_alist A l0 *)
  rewrite H7.  cut
   (MapGet A m0 ((fun a0 : ad => Ndiv2 (fp a0)) a) = Some y /\
    (fun a0 : ad => pf (Ndouble a0)) ((fun a0 : ad => Ndiv2 (fp a0)) a) =
    a).
(* Goal: and (@eq bool match MapGet B m3 (N.div2 (fp a)) with | Some a => true | None => false end false) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro H8.  split.  exact (proj1 H8).  replace (fp a) with (fp (pf (Ndouble (Ndiv2 (fp a))))).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (H1 (Ndouble (Ndiv2 (fp a)))).  assumption.  rewrite (proj2 H8).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  reflexivity.  exact
   (H (fun a0 : ad => pf (Ndouble a0)) (fun a0 : ad => Ndiv2 (fp a0)) H4
      a y H3).
(* Goal: forall _ : and (@eq bool (in_dom A (fp a1) (MapRemove A (M2 A m0 m1) a)) true) (@eq ad (pf (fp a1)) a1), or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a1) (M1 B a a0)) false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m) false) (@eq ad (pf (fp a)) a)))) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m2) false) (@eq ad (pf (fp a)) a)))) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2))), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m m2)) false) (@eq ad (pf (fp a)) a))) *)
  intro a0.  rewrite (H1 (Ndouble a0)).  apply Ndouble_div2.  intro H3.
(* Goal: and (@eq (option A) (MapGet A (M2 A m0 m1) (fp a)) (@Some A y)) (@eq ad (pf (fp a)) a) *)
  fold (aapp A) in H3.  rewrite (MapGet_M2_bit_0_if A m0 m1 (fp a)).
(* Goal: forall _ : forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a, no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble_plus_one a))) = a).
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intro H4.  elim
   (H0 (fun a0 : ad => pf (Ndouble_plus_one a0))
      (fun a0 : ad => Ndiv2 (fp a0)) H4 a y H3).
(* Goal: forall (_ : @eq (option A) (MapGet A m1 (N.div2 (fp a))) (@Some A y)) (_ : @eq ad (pf (N.succ_double (N.div2 (fp a)))) a), and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intros H5 H6.  elim (sumbool_of_bool (Nbit0 (fp a))).  intro H7.  rewrite H7.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  split.  assumption.  rewrite (Ndiv2_double_plus_one (fp a) H7) in H6.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  intro H7.  cut (Neqb (Ndouble_plus_one (Ndiv2 (fp a))) (fp a) = false).
(* Goal: forall _ : @eq bool (N.eqb (N.succ_double (N.div2 (fp a))) (fp a)) false, and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: @eq bool (N.eqb (N.succ_double (N.div2 (fp a))) (fp a)) false *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  cut (fp (pf (Ndouble_plus_one (Ndiv2 (fp a)))) = fp a).  rewrite (H1 (Ndouble_plus_one (Ndiv2 (fp a)))).
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros H8 H9.  rewrite H8 in H9.  rewrite (Neqb_correct (fp a)) in H9.  discriminate.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite H6.  reflexivity.  apply Neven_not_double_plus_one.  assumption.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro a0.  rewrite (H1 (Ndouble_plus_one a0)).  apply Ndouble_plus_one_div2.
Qed.

Lemma my_alist_of_map_lemma_3 :
 forall (A : Set) (m : Map A) (a : ad) (y : A),
 In (a, y) (alist_of_Map _ m) -> MapGet _ m a = Some y.
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold alist_of_Map in |- *.  unfold MapFold in |- *.  intros.  cut (forall a : ad, (fun a0 : ad => a0) ((fun a0 : ad => a0) a) = a).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro.  elim
   (my_alist_of_map_lemma_2 A _ (fun a0 : ad => a0) 
      (fun a0 : ad => a0) H0 _ _ H).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros; assumption.  reflexivity.
Qed.

Definition f_OK (A B : Set) (f : ad -> A -> Map B) :=
  forall (a a1 a2 : ad) (y1 y2 : A),
  in_dom _ a (f a1 y1) = true -> in_dom _ a (f a2 y2) = true -> a1 = a2.

Definition no_dup_alist (A : Set) (l : alist A) :=
  forall (a : ad) (y1 y2 : A), In (a, y1) l -> In (a, y2) l -> y1 = y2.

Lemma no_dup_alist_of_Map :
 forall (A : Set) (m : Map A), no_dup_alist _ (alist_of_Map _ m).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold no_dup_alist in |- *.  intros.  cut (MapGet _ m a = Some y1).  intros.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  cut (MapGet _ m a = Some y2).  intros.  rewrite H1 in H2.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  injection H2; intros; assumption.  apply my_alist_of_map_lemma_3.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  apply my_alist_of_map_lemma_3.  assumption.  
Qed.

Lemma my_fold_right_lemma :
 forall (A B : Set) (f : ad -> A -> Map B) (l : alist A),
 f_OK _ _ f ->
 no_dup_alist _ l ->
 forall (a : ad) (y : B),
 MapGet _
   (fold_right
      (fun (r : ad * A) (m0 : Map B) =>
       let (a0, y0) := r in MapMerge B (f a0 y0) m0) 
      (M0 B) l) a = Some y <->
 (exists a1 : ad,
    (exists y1 : A, In (a1, y1) l /\ MapGet _ (f a1 y1) a = Some y)).
Proof.
(* Goal: forall (A B : Set) (f : forall (_ : ad) (_ : A), Map B) (l : alist A) (_ : f_OK A B f) (_ : no_dup_alist A l) (a : ad) (y : B), iff (@eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l) a) (@Some B y)) (@ex ad (fun a1 : ad => @ex A (fun y1 : A => and (@In (prod ad A) (@pair ad A a1 y1) l) (@eq (option B) (MapGet B (f a1 y1) a) (@Some B y))))) *)
  simple induction l.  simpl in |- *.  split.  intro; discriminate.  intro H1.  inversion H1.
(* Goal: forall (a : ad) (b : A), R (@fold_right M (prod ad A) (F A f) neutral (aapp A (@cons (prod ad A) (@pair ad A a b) l0) l')) (op (@fold_right M (prod ad A) (F A f) neutral (@cons (prod ad A) (@pair ad A a b) l0)) (@fold_right M (prod ad A) (F A f) neutral l')) *)
  inversion H2.  elim H3; tauto.  intro a.  elim a.  clear a; intros a y.
(* Goal: and (@eq bool match MapGet B m3 (N.div2 (fp a)) with | Some a => true | None => false end false) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros l0 H H0 H1 a0 y0.  cut (no_dup_alist _ l0).  intro H2.  split.  intro H3.  simpl in H3.
  rewrite
   (MapMerge_semantics B (f a y)
      (fold_right
         (fun (r : ad * A) (m0 : Map B) =>
          let (a1, y1) := r in MapMerge B (f a1 y1) m0) 
         (M0 B) l0) a0) in H3.
  elim
   (option_sum _
      (MapGet B
         (fold_right
            (fun (r : ad * A) (m0 : Map B) =>
             let (a1, y1) := r in MapMerge B (f a1 y1) m0) 
            (M0 B) l0) a0)).
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intro H4.  elim H4; clear H4.  intros x H4.  elim (proj1 (H H0 H2 a0 x) H4).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros x0 H5.  elim H5; clear H5; intros.  split with x0.  split with x1.  split.
(* Goal: @In (prod ad A) (@pair ad A a1 y2) (@cons (prod ad A) (@pair ad A a y) l0) *)
  apply in_cons.  exact (proj1 H5).  rewrite H4 in H3.  injection H3; intro H6.
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  rewrite <- H6.  exact (proj2 H5).  intro H4.  rewrite H4 in H3.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  split with a.  split with y.  split.  apply in_eq.  assumption.  intro H3.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  elim H3; clear H3.  intros a1 H3.  elim H3; clear H3.  intros y1 H3.  simpl in |- *.
(* Goal: @eq (option B) (MapGet B (MapMerge B (f a y) (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l0)) a0) (@Some B y0) *)
(* Goal: no_dup_alist A l0 *)
  elim H3; clear H3; intros H3 H4.  elim (in_inv H3).  intro H5.
(* Goal: forall (_ : @eq (option A) (MapGet A m1 (N.div2 (fp a))) (@Some A y)) (_ : @eq ad (pf (N.succ_double (N.div2 (fp a)))) a), and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  injection H5; clear H5; intros H5 H6.  rewrite
   (MapMerge_semantics B (f a y)
      (fold_right
         (fun (r : ad * A) (m0 : Map B) =>
          let (a1, y1) := r in MapMerge B (f a1 y1) m0) 
         (M0 B) l0) a0).
  elim
   (option_sum _
      (MapGet B
         (fold_right
            (fun (r : ad * A) (m0 : Map B) =>
             let (a1, y1) := r in MapMerge B (f a1 y1) m0) 
            (M0 B) l0) a0)).
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp (pf (N.succ_double a)))) m0) true) (@eq ad (pf (N.double (N.div2 (fp (pf (N.succ_double a)))))) (pf (N.succ_double a))), False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro H7.  elim H7.  clear H7.  intros x H7.  rewrite H7.  elim (proj1 (H H0 H2 a0 x) H7).
(* Goal: forall (_ : @eq ad (N.succ_double (N.div2 (fp a))) (fp a)) (_ : @eq bool (N.eqb (N.succ_double (N.div2 (fp a))) (fp a)) false), and (@eq (option A) (if N.odd (fp a) then MapGet A m1 (N.div2 (fp a)) else MapGet A m0 (N.div2 (fp a))) (@Some A y)) (@eq ad (pf (fp a)) a) *)
(* Goal: @eq ad (fp (pf (N.succ_double (N.div2 (fp a))))) (fp a) *)
(* Goal: @eq bool (N.eqb (N.succ_double (N.div2 (fp a))) (fp a)) false *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intros x0 H8.  elim H8; clear H8; intros x1 H8.  elim H8; clear H8; intros H8 H9.
(* Goal: @eq (option B) (@Some B x) (@Some B y0) *)
(* Goal: forall _ : @eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0) (@None B), @eq (option B) match MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0 with | Some y' => @Some B y' | None => MapGet B (f a y) a0 end (@Some B y0) *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a1 y1) l0, @eq (option B) (MapGet B (MapMerge B (f a y) (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l0)) a0) (@Some B y0) *)
(* Goal: no_dup_alist A l0 *)
  unfold f_OK in H0.  cut (a1 = x0).  intro H10.  rewrite <- H10 in H8.
(* Goal: @eq (option B) (@Some B x) (@Some B y0) *)
(* Goal: @eq ad a1 x0 *)
(* Goal: forall _ : @eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0) (@None B), @eq (option B) match MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0 with | Some y' => @Some B y' | None => MapGet B (f a y) a0 end (@Some B y0) *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a1 y1) l0, @eq (option B) (MapGet B (MapMerge B (f a y) (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l0)) a0) (@Some B y0) *)
(* Goal: no_dup_alist A l0 *)
  cut (In (a1, x1) ((a, y) :: l0)).  intro H11.  unfold no_dup_alist in H1.
(* Goal: @eq (option B) (@Some B x) (@Some B y0) *)
(* Goal: @In (prod ad A) (@pair ad A a1 x1) (@cons (prod ad A) (@pair ad A a y) l0) *)
(* Goal: @eq ad a1 x0 *)
(* Goal: forall _ : @eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0) (@None B), @eq (option B) match MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a1, y1) := r in MapMerge B (f a1 y1) m0) (M0 B) l0) a0 with | Some y' => @Some B y' | None => MapGet B (f a y) a0 end (@Some B y0) *)
(* Goal: forall _ : @In (prod ad A) (@pair ad A a1 y1) l0, @eq (option B) (MapGet B (MapMerge B (f a y) (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) l0)) a0) (@Some B y0) *)
(* Goal: no_dup_alist A l0 *)
  rewrite <- (H1 _ _ _ H3 H11) in H9.  rewrite <- H10 in H9.  rewrite H4 in H9.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  symmetry  in |- *; assumption.  apply in_cons.  assumption.  apply H0 with (a := a0) (y1 := y1) (y2 := x1).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  unfold in_dom in |- *.  rewrite H4.  reflexivity.  unfold in_dom in |- *.  rewrite H9.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  reflexivity.  intro H7.  rewrite H7.  rewrite H5.  rewrite H6.  assumption.  intro H5.
  rewrite
   (MapMerge_semantics B (f a y)
      (fold_right
         (fun (r : ad * A) (m0 : Map B) =>
          let (a1, y1) := r in MapMerge B (f a1 y1) m0) 
         (M0 B) l0) a0).
  cut
   (MapGet B
      (fold_right
         (fun (r : ad * A) (m0 : Map B) =>
          let (a1, y1) := r in MapMerge B (f a1 y1) m0) 
         (M0 B) l0) a0 = Some y0).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  intro H6.  rewrite H6.  reflexivity.  apply (proj2 (H H0 H2 a0 y0)).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  split with a1.  split with y1.  split; assumption.  unfold no_dup_alist in |- *.
(* Goal: @In (prod ad A) (@pair ad A a1 y2) (@cons (prod ad A) (@pair ad A a y) l0) *)
  intros a1 y1 y2 H2 H3.  unfold no_dup_alist in H1.  refine (H1 a1 y1 y2 _ _).  apply in_cons.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  apply in_cons.  assumption.
Qed.

(* Finally, the semantics of MapFold which we will be using *)

Lemma myMapFold_lemma :
 forall (A B : Set) (f : ad -> A -> Map B) (m : Map A),
 f_OK _ _ f ->
 forall (a : ad) (y : B),
 MapGet _ (MapFold _ _ (M0 _) (MapMerge _) f m) a = Some y <->
 (exists a1 : ad,
    (exists y1 : A,
       MapGet _ m a1 = Some y1 /\ MapGet _ (f a1 y1) a = Some y)).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  rewrite (myMapFold_as_fold_2 _ _ f m a).  cut (no_dup_alist _ (alist_of_Map _ m)).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro.  split.  intro.  elim (proj1 (my_fold_right_lemma _ _ f (alist_of_Map _ m) H H0 a y)).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  inversion H2.  split with x.  split with x0.  split.
(* Goal: @eq (option A) (MapGet A m x) (@Some A x0) *)
(* Goal: @eq (option B) (MapGet B (f x x0) a) (@Some B y) *)
(* Goal: @eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m0 : Map B) => let (a0, y0) := r in MapMerge B (f a0 y0) m0) (M0 B) (alist_of_Map A m)) a) (@Some B y) *)
(* Goal: forall _ : @ex ad (fun a1 : ad => @ex A (fun y1 : A => and (@eq (option A) (MapGet A m a1) (@Some A y1)) (@eq (option B) (MapGet B (f a1 y1) a) (@Some B y)))), @eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m : Map B) => let (a, y) := r in MapMerge B (f a y) m) (M0 B) (alist_of_Map A m)) a) (@Some B y) *)
(* Goal: no_dup_alist A (alist_of_Map A m) *)
  apply my_alist_of_map_lemma_3.  exact (proj1 H3).  exact (proj2 H3).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  intro.  inversion H1.  inversion H2.
(* Goal: @eq (option B) (MapGet B (@fold_right (Map B) (prod ad A) (fun (r : prod ad A) (m : Map B) => let (a, y) := r in MapMerge B (f a y) m) (M0 B) (alist_of_Map A m)) a) (@Some B y) *)
(* Goal: no_dup_alist A (alist_of_Map A m) *)
  elim (proj2 (my_fold_right_lemma _ _ f (alist_of_Map _ m) H H0 a y)).
(* Goal: and (@eq bool match MapGet B m3 (N.div2 (fp a)) with | Some a => true | None => false end false) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  reflexivity.  split with x.  split with x0.  split.  apply my_alist_of_map_lemma_1.
(* Goal: @eq (option A) (MapGet A m x) (@Some A x0) *)
(* Goal: @eq (option B) (MapGet B (f x x0) a) (@Some B y) *)
(* Goal: no_dup_alist A (alist_of_Map A m) *)
  exact (proj1 H3).  exact (proj2 H3).  apply no_dup_alist_of_Map.
Qed.


Section My_Map.

Variable A B : Set.

Fixpoint Mapn (n : nat) : Set :=
  match n with
  | O => A
  | S m => Map (Mapn m)
  end.

(* Left to define MapGetn, MapPutn, MapPutn_semantics ... *)
      
Definition MapGet2 (m : Map (Map A)) (a b : ad) :=
  match MapGet _ m a with
  | None => None 
  | Some m' => MapGet _ m' b
  end.

Definition MapGet3 (m : Map (Map (Map A))) (a b c : ad) :=
  match MapGet _ m a with
  | None => None
  | Some m' => MapGet2 m' b c
  end.

Definition MapPut2 (m : Map (Map A)) (a b : ad) (c : A) :=
  match MapGet _ m a with
  | Some m' => MapPut _ m a (MapPut _ m' b c)
  | None => MapPut _ m a (M1 _ b c)
  end.

Definition MapPut3 (m : Map (Map (Map A))) (a b c : ad) 
  (d : A) :=
  match MapGet _ m a with
  | Some m' => MapPut _ m a (MapPut2 m' b c d)
  | None => MapPut _ m a (M1 _ b (M1 _ c d))
  end.

Lemma MapPut2_semantics :
 forall (m : Map (Map A)) (a b a1 b1 : ad) (c : A),
 MapGet2 (MapPut2 m a b c) a1 b1 =
 (if Neqb a a1 && Neqb b b1 then Some c else MapGet2 m a1 b1).
Proof.
(* Goal: forall (m : Map (Map A)) (a b a1 b1 : ad) (c : A), @eq (option A) (MapGet2 (MapPut2 m a b c) a1 b1) (if andb (N.eqb a a1) (N.eqb b b1) then @Some A c else MapGet2 m a1 b1) *)
  intros m a b a1 b1 c.  unfold MapGet2, MapPut2 in |- *.  elim (option_sum _ (MapGet (Map A) m a)).
(* Goal: @eq (option A) match (if N.eqb b b1 then @Some (Map A) (M1 A c d) else @None (Map A)) with | Some m' => MapGet A m' c1 | None => @None A end (if andb (N.eqb b b1) (N.eqb c c1) then @Some A d else match MapGet (Map (Map A)) m a with | Some m' => match MapGet (Map A) m' b1 with | Some m'0 => MapGet A m'0 c1 | None => @None A end | None => @None A end) *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @eq (option A) match (if N.eqb a a1 then @Some (Map (Map A)) (M1 (Map A) b (M1 A c d)) else MapGet (Map (Map A)) m a1) with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
  intro H.  elim H; clear H; intros x H.  rewrite H.
(* Goal: @eq (option A) match MapGet (Map A) (MapPut (Map A) m a (MapPut A x b c)) a1 with | Some m' => MapGet A m' b1 | None => @None A end (if andb (N.eqb a a1) (N.eqb b b1) then @Some A c else match MapGet (Map A) m a1 with | Some m' => MapGet A m' b1 | None => @None A end) *)
(* Goal: forall _ : @eq (option (Map A)) (MapGet (Map A) m a) (@None (Map A)), @eq (option A) match MapGet (Map A) match MapGet (Map A) m a with | Some m' => MapPut (Map A) m a (MapPut A m' b c) | None => MapPut (Map A) m a (M1 A b c) end a1 with | Some m' => MapGet A m' b1 | None => @None A end (if andb (N.eqb a a1) (N.eqb b b1) then @Some A c else match MapGet (Map A) m a1 with | Some m' => MapGet A m' b1 | None => @None A end) *)
  rewrite (MapPut_semantics (Map A) m a (MapPut A x b c) a1).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  elim (sumbool_of_bool (Neqb a a1)).  intro H0.  rewrite H0.  simpl in |- *.
(* Goal: @eq (option A) (MapGet A (MapPut A x b c) b1) (if N.eqb b b1 then @Some A c else match MapGet (Map A) m a1 with | Some m' => MapGet A m' b1 | None => @None A end) *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @eq (option A) match (if N.eqb a a1 then @Some (Map A) (MapPut A x b c) else MapGet (Map A) m a1) with | Some m' => MapGet A m' b1 | None => @None A end (if andb (N.eqb a a1) (N.eqb b b1) then @Some A c else match MapGet (Map A) m a1 with | Some m' => MapGet A m' b1 | None => @None A end) *)
(* Goal: forall _ : @eq (option (Map A)) (MapGet (Map A) m a) (@None (Map A)), @eq (option A) match MapGet (Map A) match MapGet (Map A) m a with | Some m' => MapPut (Map A) m a (MapPut A m' b c) | None => MapPut (Map A) m a (M1 A b c) end a1 with | Some m' => MapGet A m' b1 | None => @None A end (if andb (N.eqb a a1) (N.eqb b b1) then @Some A c else match MapGet (Map A) m a1 with | Some m' => MapGet A m' b1 | None => @None A end) *)
  rewrite (MapPut_semantics A x b c b1).  rewrite <- (Neqb_complete a a1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite H.  reflexivity.  assumption.  intro H0.  rewrite H0.  simpl in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  reflexivity.  intro H.  rewrite H.  simpl in |- *.  elim (sumbool_of_bool (Neqb a a1)).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  intro H0.  rewrite H0.  simpl in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  rewrite (MapPut_semantics (Map A) m a (M1 A b c) a1).  rewrite H0.  simpl in |- *.
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite <- (Neqb_complete _ _ H0).  rewrite H.  reflexivity.  intro H0.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  rewrite H0.  simpl in |- *.  rewrite (MapPut_semantics (Map A) m a (M1 A b c) a1).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite H0.  reflexivity.
Qed.
 
Lemma MapPut3_semantics :
 forall (m : Map (Map (Map A))) (a b c a1 b1 c1 : ad) (d : A),
 MapGet3 (MapPut3 m a b c d) a1 b1 c1 =
 (if Neqb a a1 && (Neqb b b1 && Neqb c c1)
  then Some d
  else MapGet3 m a1 b1 c1).
Proof.
(* Goal: forall (m : Map (Map (Map A))) (a b c a1 b1 c1 : ad) (d : A), @eq (option A) (MapGet3 (MapPut3 m a b c d) a1 b1 c1) (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else MapGet3 m a1 b1 c1) *)
  intros m a b c a1 b1 c1 d.  unfold MapGet3, MapPut3 in |- *.
(* Goal: forall _ : @eq (option (Map (Map A))) (MapGet (Map (Map A)) m a) (@None (Map (Map A))), @eq (option A) match MapGet (Map (Map A)) match MapGet (Map (Map A)) m a with | Some m' => MapPut (Map (Map A)) m a (MapPut2 m' b c d) | None => MapPut (Map (Map A)) m a (M1 (Map A) b (M1 A c d)) end a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
  elim (option_sum _ (MapGet (Map (Map A)) m a)).  intro H.
(* Goal: @eq (option A) match (if N.eqb b b1 then @Some (Map A) (M1 A c d) else @None (Map A)) with | Some m' => MapGet A m' c1 | None => @None A end (if andb (N.eqb b b1) (N.eqb c c1) then @Some A d else match MapGet (Map (Map A)) m a with | Some m' => match MapGet (Map A) m' b1 with | Some m'0 => MapGet A m'0 c1 | None => @None A end | None => @None A end) *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @eq (option A) match (if N.eqb a a1 then @Some (Map (Map A)) (M1 (Map A) b (M1 A c d)) else MapGet (Map (Map A)) m a1) with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
  elim H; clear H; intros x H.  rewrite H.
(* Goal: @eq (option A) match MapGet (Map (Map A)) (MapPut (Map (Map A)) m a (MapPut2 x b c d)) a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
(* Goal: forall _ : @eq (option (Map (Map A))) (MapGet (Map (Map A)) m a) (@None (Map (Map A))), @eq (option A) match MapGet (Map (Map A)) match MapGet (Map (Map A)) m a with | Some m' => MapPut (Map (Map A)) m a (MapPut2 m' b c d) | None => MapPut (Map (Map A)) m a (M1 (Map A) b (M1 A c d)) end a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
  rewrite (MapPut_semantics (Map (Map A)) m a (MapPut2 x b c d) a1).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  elim (sumbool_of_bool (Neqb a a1)).  intro H0.  rewrite H0.  simpl in |- *.
(* Goal: @eq (option A) match (if N.eqb b b1 then @Some (Map A) (M1 A c d) else @None (Map A)) with | Some m' => MapGet A m' c1 | None => @None A end (if andb (N.eqb b b1) (N.eqb c c1) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => match MapGet (Map A) m' b1 with | Some m'0 => MapGet A m'0 c1 | None => @None A end | None => @None A end) *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @eq (option A) match (if N.eqb a a1 then @Some (Map (Map A)) (M1 (Map A) b (M1 A c d)) else MapGet (Map (Map A)) m a1) with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
  rewrite <- (Neqb_complete _ _ H0).  rewrite (MapPut2_semantics x b c b1 c1 d).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  rewrite H.  reflexivity.  intro H0.  rewrite H0.  simpl in |- *.  reflexivity.  intro H.
(* Goal: @eq (option A) match (if N.eqb b b1 then @Some (Map A) (M1 A c d) else @None (Map A)) with | Some m' => MapGet A m' c1 | None => @None A end (if andb (N.eqb b b1) (N.eqb c c1) then @Some A d else match MapGet (Map (Map A)) m a with | Some m' => match MapGet (Map A) m' b1 with | Some m'0 => MapGet A m'0 c1 | None => @None A end | None => @None A end) *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @eq (option A) match (if N.eqb a a1 then @Some (Map (Map A)) (M1 (Map A) b (M1 A c d)) else MapGet (Map (Map A)) m a1) with | Some m' => MapGet2 m' b1 c1 | None => @None A end (if andb (N.eqb a a1) (andb (N.eqb b b1) (N.eqb c c1)) then @Some A d else match MapGet (Map (Map A)) m a1 with | Some m' => MapGet2 m' b1 c1 | None => @None A end) *)
  rewrite H.  rewrite (MapPut_semantics (Map (Map A)) m a (M1 (Map A) b (M1 A c d)) a1).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  elim (sumbool_of_bool (Neqb a a1)).  intro H0.  rewrite H0.  simpl in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  unfold MapGet2 in |- *.  simpl in |- *.  rewrite <- (Neqb_complete _ _ H0).  rewrite H.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  elim (Neqb b b1).  simpl in |- *.  reflexivity.  simpl in |- *.  reflexivity.  intro H0.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  rewrite H0.  simpl in |- *.  reflexivity.
Qed.

Lemma makeM2_MapDom_lemma :
 forall (A : Set) (m1 m2 : Map A),
 makeM2 unit (MapDom A m1) (MapDom A m2) = MapDom A (makeM2 A m1 m2).
Proof.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  intro.  simple induction m1.  simpl in |- *.  simple induction m2.  simpl in |- *.  reflexivity.  simpl in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  reflexivity.  simpl in |- *.  reflexivity.  intro.  intro.  simple induction m2.  simpl in |- *.
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  reflexivity.  reflexivity.  reflexivity.  reflexivity.
Qed.

Fixpoint MapDomRestrTo_DomBy (m : Map A) : Map B -> Map A * Map unit :=
  match m with
  | M0 => fun _ : Map B => (M0 A, M0 unit)
  | M1 a y =>
      fun m' : Map B =>
      match MapGet B m' a with
      | None => (M0 A, M1 unit a tt)
      | _ => (m, M0 unit)
      end
  | M2 m1 m2 =>
      fun m' : Map B =>
      match m' with
      | M0 => (M0 A, MapDom A m)
      | M1 a' y' =>
          (match MapGet A m a' with
           | None => M0 A
           | Some y => M1 A a' y
           end, MapDom A (MapRemove A m a'))
      | M2 m'1 m'2 =>
          match MapDomRestrTo_DomBy m1 m'1 with
          | (x1, y1) =>
              match MapDomRestrTo_DomBy m2 m'2 with
              | (x2, y2) => (makeM2 A x1 x2, makeM2 unit y1 y2)
              end
          end
      end
  end.

Lemma MapDomRestrTo_DomBy_lemma_1 :
 forall (m : Map A) (m' : Map B),
 fst (MapDomRestrTo_DomBy m m') = MapDomRestrTo A B m m'.
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  reflexivity.  simpl in |- *.  intros.  elim (MapGet B m' a).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  reflexivity.  reflexivity.  simpl in |- *.  intro.  intro.  intro.  intro.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m'.  reflexivity.  reflexivity.  intros.  rewrite <- (H m2).
(* Goal: @eq (Map A) (@fst (Map A) (Map unit) (let (x1, y1) := MapDomRestrTo_DomBy m0 m2 in let (x2, y2) := MapDomRestrTo_DomBy m1 m3 in @pair (Map A) (Map unit) (makeM2 A x1 x2) (makeM2 unit y1 y2))) (makeM2 A (@fst (Map A) (Map unit) (MapDomRestrTo_DomBy m0 m2)) (MapDomRestrTo A B m1 m3)) *)
  rewrite <- (H0 m3).  elim (MapDomRestrTo_DomBy m0 m2).  elim (MapDomRestrTo_DomBy m1 m3).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
reflexivity.
Qed.

Lemma MapDomRestrTo_DomBy_lemma_2 :
 forall (m : Map A) (m' : Map B),
 snd (MapDomRestrTo_DomBy m m') = MapDom A (MapDomRestrBy A B m m').
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  reflexivity.  intros.  simpl in |- *.  unfold MapDom in |- *.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (MapGet B m' a).  reflexivity.  reflexivity.  intro.  intro.  intro.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro.  simple induction m'.  reflexivity.  reflexivity.  intros.  simpl in |- *.
(* Goal: @eq (Map unit) (@snd (Map A) (Map unit) (let (x1, y1) := MapDomRestrTo_DomBy m0 m2 in let (x2, y2) := MapDomRestrTo_DomBy m1 m3 in @pair (Map A) (Map unit) (makeM2 A x1 x2) (makeM2 unit y1 y2))) (MapDom A (makeM2 A (MapDomRestrBy A B m0 m2) (MapDomRestrBy A B m1 m3))) *)
  cut (snd (MapDomRestrTo_DomBy m0 m2) = MapDom A (MapDomRestrBy A B m0 m2)).
(* Goal: forall _ : @eq (Map unit) (@snd (Map A) (Map unit) (MapDomRestrTo_DomBy m0 m2)) (MapDom A (MapDomRestrBy A B m0 m2)), @eq (Map unit) (@snd (Map A) (Map unit) (let (x1, y1) := MapDomRestrTo_DomBy m0 m2 in let (x2, y2) := MapDomRestrTo_DomBy m1 m3 in @pair (Map A) (Map unit) (makeM2 A x1 x2) (makeM2 unit y1 y2))) (MapDom A (makeM2 A (MapDomRestrBy A B m0 m2) (MapDomRestrBy A B m1 m3))) *)
(* Goal: @eq (Map unit) (@snd (Map A) (Map unit) (MapDomRestrTo_DomBy m0 m2)) (MapDom A (MapDomRestrBy A B m0 m2)) *)
  cut (snd (MapDomRestrTo_DomBy m1 m3) = MapDom A (MapDomRestrBy A B m1 m3)).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (MapDomRestrTo_DomBy m1 m3).  elim (MapDomRestrTo_DomBy m0 m2).  intros.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simpl in |- *.  simpl in H3, H4.  rewrite H3.  rewrite H4.  apply makeM2_MapDom_lemma.
(* Goal: @In ad a (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0) *)
  apply H0.  apply H.
Qed.

Fixpoint map_app_list1 (pf : ad -> ad) (l : list ad) 
 (m : Map A) {struct m} : list ad :=
  match m with
  | M0 => l
  | M1 a y => pf a :: l
  | M2 m1 m2 =>
      map_app_list1 (fun a0 : ad => pf (Ndouble_plus_one a0))
        (map_app_list1 (fun a0 : ad => pf (Ndouble a0)) l m1) m2
  end.

Lemma map_app_list1_lemma_1 :
 forall (m : Map A) (pf : ad -> ad) (l : list ad) (a : ad),
 In a l -> In a (map_app_list1 pf l m).
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  tauto.  simpl in |- *.  tauto.  simpl in |- *.  intros.  apply H0.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H.  assumption.
Qed.

Lemma map_app_list1_lemma_2 :
 forall (m : Map A) (pf fp : ad -> ad) (l : list ad),
 (forall a0 : ad, fp (pf a0) = a0) ->
 forall a : ad,
 In a (map_app_list1 pf l m) ->
 In a l \/ in_dom _ (fp a) m = true /\ pf (fp a) = a.
Proof.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  intros pf fp l H a H0.  left; assumption.  simpl in |- *.  intros a a0 pf fp l H a1 H0.
(* Goal: and (@eq bool (in_dom A (fp (pf a)) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp (pf a)) m') false) (@eq ad (pf (fp (pf a))) (pf a))) *)
(* Goal: forall _ : @In ad a1 l, or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp a1) m') false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m0 m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m0) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m m0) m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m m0)) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a))) *)
  elim H0; intro H2.  rewrite <- H2.  rewrite (H a).  right.  unfold in_dom in |- *.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simpl in |- *.  rewrite (Neqb_correct a).  split; reflexivity.  left; assumption.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simpl in |- *.  intros m0 H m1 H0 pf fp l H1 a H2.
(* Goal: forall _ : forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a, no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble_plus_one a))) = a).
(* Goal: forall _ : and (@eq bool (in_dom A (fp a1) (MapRemove A (M2 A m0 m1) a)) true) (@eq ad (pf (fp a1)) a1), or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a1) (M1 B a a0)) false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m) false) (@eq ad (pf (fp a)) a)))) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m2) false) (@eq ad (pf (fp a)) a)))) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2))), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m m2)) false) (@eq ad (pf (fp a)) a))) *)
  intro H3.  elim
   (H0 (fun a0 : ad => pf (Ndouble_plus_one a0))
      (fun a0 : ad => Ndiv2 (fp a0)) _ H3 a H2).
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intro H4.
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble a))) = a).
(* Goal: forall _ : forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a, or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  intro H5.  elim
   (H (fun a0 : ad => pf (Ndouble a0)) (fun a0 : ad => Ndiv2 (fp a0)) _
      H5 a H4).
(* Goal: or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a))) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  tauto.  intro H6.  elim H6; clear H6; intros H6 H7.  right.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Nbit0 (fp a))).  intro y.  rewrite <- H7 in y.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  rewrite (H1 (Ndouble (Ndiv2 (fp a)))) in y.  rewrite (Ndouble_bit0 (Ndiv2 (fp a))) in y.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  discriminate.  intro y.  unfold in_dom in |- *.  rewrite (MapGet_M2_bit_0_0 _ (fp a) y m0 m1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in H6.  split.  assumption.  rewrite (Ndiv2_double (fp a) y) in H7.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  intro a0.  rewrite (H1 (Ndouble a0)).  apply Ndouble_div2.
(* Goal: or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a))) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro H4.  elim H4; clear H4; intros H4 H5.  right.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Nbit0 (fp a))).  intro y.  unfold in_dom in |- *.
(* Goal: and (@eq bool match MapGet B m3 (N.div2 (fp a)) with | Some a => true | None => false end false) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (MapGet_M2_bit_0_1 _ (fp a) y m0 m1).  unfold in_dom in H4.  split.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  rewrite (Ndiv2_double_plus_one _ y) in H5.  assumption.  intro y.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (@eq ad (pf (fp a)) a) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
  rewrite <- H5 in y.  rewrite (H1 (Ndouble_plus_one (Ndiv2 (fp a)))) in y.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_bit0 (Ndiv2 (fp a))) in y.  discriminate.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro a0.  rewrite (H1 (Ndouble_plus_one a0)).  apply Ndouble_plus_one_div2.
Qed.

Lemma map_app_list1_lemma_3 :
 forall (m : Map A) (pf fp : ad -> ad) (l : list ad),
 (forall a0 : ad, fp (pf a0) = a0) ->
 no_dup_list _ l ->
 (forall a : ad, in_dom _ a m = true -> ~ In (pf a) l) ->
 no_dup_list _ (map_app_list1 pf l m).
Proof.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simple induction m.  simpl in |- *.  tauto.  simpl in |- *.  intros a a0 pf fp l H H0 H1.  apply no_dup_cons.  unfold not in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  intro H2.  absurd (In (pf a) l).  apply H1 with (a1 := a).  unfold in_dom in |- *.  simpl in |- *.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Neqb_correct a).  reflexivity.  assumption.  assumption.  simpl in |- *.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros m0 H m1 H0 pf fp l H1 H2 H3.  apply H0 with (fp := fun a0 : ad => Ndiv2 (fp a0)).  intro a0.
(* Goal: @eq ad (N.div2 (fp (pf (N.succ_double a0)))) a0 *)
(* Goal: no_dup_list ad (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0) *)
(* Goal: forall (a : ad) (_ : @eq bool (in_dom A a m1) true), not (@In ad (pf (N.succ_double a)) (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0)) *)
  rewrite (H1 (Ndouble_plus_one a0)).  apply Ndouble_plus_one_div2.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H with (fp := fun a0 : ad => Ndiv2 (fp a0)).  intro a0.  rewrite (H1 (Ndouble a0)).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply Ndouble_div2.  assumption.  intros a H4.  apply H3.  unfold in_dom in |- *.
(* Goal: @eq bool match MapGet A (M2 A m0 m1) (N.double a) with | Some a => true | None => false end true *)
(* Goal: forall (a : ad) (_ : @eq bool (in_dom A a m1) true), not (@In ad (pf (N.succ_double a)) (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0)) *)
  rewrite (MapGet_M2_bit_0_0 _ (Ndouble a) (Ndouble_bit0 _) m0 m1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_div2 a).  assumption.  intros a H4.  unfold not in |- *; intro H5.
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble a))) = a).
(* Goal: forall _ : forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a, False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro H6.  elim
   (map_app_list1_lemma_2 m0 (fun a0 : ad => pf (Ndouble a0))
      (fun a0 : ad => Ndiv2 (fp a0)) l H6 _ H5).
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp (pf (N.succ_double a)))) m0) true) (@eq ad (pf (N.double (N.div2 (fp (pf (N.succ_double a)))))) (pf (N.succ_double a))), False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold not in H3.  intro H7.  apply H3 with (a := Ndouble_plus_one a).
(* Goal: @eq bool (in_dom B (N.double a) (M2 B m2 m3)) false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in |- *.  rewrite
   (MapGet_M2_bit_0_1 _ (Ndouble_plus_one a) (Ndouble_plus_one_bit0 _) m0
      m1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_div2 a).  assumption.  assumption.  intro H7.
(* Goal: False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim H7; clear H7; intros H7 H8.  rewrite (H1 (Ndouble_plus_one a)) in H8.
(* Goal: False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_div2 a) in H8.  elim (sumbool_of_bool (Nbit0 (Ndouble a))).
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro y.  rewrite (Ndouble_bit0 a) in y.  discriminate.  intro y.
(* Goal: False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite <- (H1 (Ndouble a)) in y.  rewrite H8 in y.
(* Goal: False *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (H1 (Ndouble_plus_one a)) in y.  rewrite (Ndouble_plus_one_bit0 a) in y.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  discriminate.  intro a0.  rewrite (H1 (Ndouble a0)).  apply Ndouble_div2.
Qed.

Lemma map_app_list1_lemma_4 :
 forall (m : Map A) (pf : ad -> ad) (l : list ad) (a : ad),
 in_dom _ a m = true -> In (pf a) (map_app_list1 pf l m).
Proof.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simple induction m.  simpl in |- *.  unfold in_dom in |- *.  simpl in |- *.  intros; discriminate.  simpl in |- *.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  unfold in_dom in H.  simpl in H.  elim (sumbool_of_bool (Neqb a a1)).
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  intro y.  rewrite y in H.  rewrite (Neqb_complete _ _ y).  left.  reflexivity.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro y.  rewrite y in H.  discriminate.  simpl in |- *.  intros.
(* Goal: forall _ : @eq bool (N.odd (N.double a)) true, False *)
(* Goal: forall _ : @eq bool (N.odd (N.double a)) false, False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Nbit0 a)).  intro y.  unfold in_dom in H1.
(* Goal: @In ad (pf a) (map_app_list1 (fun a0 : ad => pf (N.succ_double a0)) (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0) m1) *)
(* Goal: forall _ : @eq bool (N.odd a) false, @In ad (pf a) (map_app_list1 (fun a0 : ad => pf (N.succ_double a0)) (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0) m1) *)
  rewrite (MapGet_M2_bit_0_1 _ a y m0 m1) in H1.
  replace (pf a) with
   ((fun a0 : ad => pf (Ndouble_plus_one a0)) (Ndiv2 a)).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H0 with (pf := fun a0 : ad => pf (Ndouble_plus_one a0)).  assumption.  
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndiv2_double_plus_one a).  reflexivity.  assumption.  intro y.
(* Goal: @In ad (pf a) (map_app_list1 (fun a0 : ad => pf (N.succ_double a0)) (map_app_list1 (fun a0 : ad => pf (N.double a0)) l m0) m1) *)
  apply map_app_list1_lemma_1.  replace (pf a) with (pf (Ndouble (Ndiv2 a))).
(* Goal: @eq bool (in_dom B (N.double a) (M2 B m2 m3)) false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H with (pf := fun a0 : ad => pf (Ndouble a0)).  unfold in_dom in |- *.
(* Goal: @eq bool match MapGet A m0 (N.div2 a) with | Some a => true | None => false end true *)
(* Goal: @eq ad (pf (N.double (N.div2 a))) (pf a) *)
  unfold in_dom in H1.  rewrite (MapGet_M2_bit_0_0 _ _ y m0 m1) in H1.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  rewrite (Ndiv2_double _ y).  reflexivity.  
Qed.

Fixpoint MapDomRestrByApp1 (pf : ad -> ad) (l : list ad) 
 (m : Map A) {struct m} : Map B -> list ad :=
  match m with
  | M0 => fun _ : Map B => l
  | M1 a y =>
      fun m' : Map B =>
      match MapGet B m' a with
      | None => pf a :: l
      | _ => l
      end
  | M2 m1 m2 =>
      fun m' : Map B =>
      match m' with
      | M0 => map_app_list1 pf l m
      | M1 a' y' => map_app_list1 pf l (MapRemove A m a')
      | M2 m'1 m'2 =>
          MapDomRestrByApp1 (fun a0 : ad => pf (Ndouble_plus_one a0))
            (MapDomRestrByApp1 (fun a0 : ad => pf (Ndouble a0)) l m1 m'1)
            m2 m'2
      end
  end.

Lemma MapDomRestrByApp1_lemma_1 :
 forall (m : Map A) (m' : Map B) (l : list ad) (pf : ad -> ad) (a : ad),
 In a l -> In a (MapDomRestrByApp1 pf l m m').
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  tauto.  simpl in |- *.  intros.  elim (MapGet B m' a).
  Focus 2.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply in_cons.  assumption.  intro.  assumption.  intros.  elim m'.  simpl in |- *.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply map_app_list1_lemma_1.  apply map_app_list1_lemma_1.  assumption.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold MapDomRestrByApp1 in |- *.  intros.  apply map_app_list1_lemma_1.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  intros.  simpl in |- *.  apply H0.  apply H.  assumption.
Qed.

Lemma MapDomRestrByApp1_lemma_2 :
 forall (m : Map A) (m' : Map B) (l : list ad) (pf : ad -> ad) (a : ad),
 in_dom _ a m = true ->
 in_dom _ a m' = false -> In (pf a) (MapDomRestrByApp1 pf l m m').
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  unfold in_dom at 1 in |- *.  simpl in |- *.  intros.  discriminate.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in |- *.  simpl in |- *.  intros.  elim (sumbool_of_bool (Neqb a a1)).  intro y.
(* Goal: @In ad (pf a1) match MapGet B m' a with | Some b => l | None => @cons ad (pf a) l end *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @In ad (pf a1) match MapGet B m' a with | Some b0 => l | None => @cons ad (pf a) l end *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a m) true) (_ : @eq bool (in_dom B a m') false), @In ad (pf a) (MapDomRestrByApp1 pf l m m')) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a m0) true) (_ : @eq bool (in_dom B a m') false), @In ad (pf a) (MapDomRestrByApp1 pf l m0 m')) (m' : Map B) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m m0)) true) (_ : @eq bool (in_dom B a m') false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m m0) m') *)
  rewrite (Neqb_complete _ _ y).  elim (option_sum _ (MapGet B m' a1)).  intro y0.
(* Goal: @In ad (pf a1) match MapGet B m' a1 with | Some b => l | None => @cons ad (pf a1) l end *)
(* Goal: forall _ : @eq (option B) (MapGet B m' a1) (@None B), @In ad (pf a1) match MapGet B m' a1 with | Some b0 => l | None => @cons ad (pf a1) l end *)
(* Goal: forall _ : @eq bool (N.eqb a a1) false, @In ad (pf a1) match MapGet B m' a with | Some b0 => l | None => @cons ad (pf a) l end *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a m) true) (_ : @eq bool (in_dom B a m') false), @In ad (pf a) (MapDomRestrByApp1 pf l m m')) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a m0) true) (_ : @eq bool (in_dom B a m') false), @In ad (pf a) (MapDomRestrByApp1 pf l m0 m')) (m' : Map B) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m m0)) true) (_ : @eq bool (in_dom B a m') false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m m0) m') *)
  inversion y0.  rewrite H1 in H0.  rewrite y in H.  discriminate.  intro y0.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  rewrite y0.  simpl in |- *.  left.  reflexivity.  intro y.  rewrite y in H.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  discriminate.  intro.  simple induction m'.  unfold MapDomRestrByApp1 in |- *.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  apply map_app_list1_lemma_4.  assumption.  intros.
(* Goal: @In ad (pf a1) (map_app_list1 pf l (MapRemove A (M2 A m0 m1) a)) *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  unfold MapDomRestrByApp1 in |- *.  unfold in_dom in H2.  simpl in H2.
(* Goal: @eq bool (in_dom B (N.double a) (M2 B m2 m3)) false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply map_app_list1_lemma_4.  unfold in_dom in |- *.
(* Goal: @eq bool match MapGet A (MapRemove A (M2 A m0 m1) a) a1 with | Some a => true | None => false end true *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf : forall _ : ad, ad) (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), @In ad (pf a) (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite (MapRemove_semantics A (M2 A m0 m1) a a1).
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Neqb a a1)).  intro y.  rewrite y in H2.  discriminate.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro y.  rewrite y.  assumption.  intros.  simpl in |- *.
(* Goal: forall _ : @eq bool (N.odd (N.double a)) true, False *)
(* Goal: forall _ : @eq bool (N.odd (N.double a)) false, False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Nbit0 a)).  intro y.  unfold in_dom in H3, H4.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall _ : @eq bool (N.odd a) false, @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  rewrite (MapGet_M2_bit_0_1 A a y m0 m1) in H3.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall _ : @eq bool (N.odd a) false, @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  rewrite (MapGet_M2_bit_0_1 B a y m2 m3) in H4.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall _ : @eq bool (N.odd a) false, @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  replace (pf a) with (pf (Ndouble_plus_one (Ndiv2 a))).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H0 with (pf := fun a0 : ad => pf (Ndouble_plus_one a0)).  assumption.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  rewrite (Ndiv2_double_plus_one _ y).  reflexivity.  intro y.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  unfold in_dom in H3, H4.  rewrite (MapGet_M2_bit_0_0 A a y m0 m1) in H3.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  rewrite (MapGet_M2_bit_0_0 B a y m2 m3) in H4.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  apply MapDomRestrByApp1_lemma_1.
(* Goal: @In ad (pf a) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
  replace (pf a) with (pf (Ndouble (Ndiv2 a))).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H with (pf := fun a0 : ad => pf (Ndouble a0)).  assumption.  assumption.  
(* Goal: @eq bool false false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite (Ndiv2_double _ y).  reflexivity.
Qed.

Lemma MapDomRestrByApp1_lemma_3 :
 forall (m : Map A) (m' : Map B) (l : list ad) (pf fp : ad -> ad),
 (forall a : ad, fp (pf a) = a) ->
 forall a : ad,
 In a (MapDomRestrByApp1 pf l m m') ->
 In a l \/
 in_dom _ (fp a) m = true /\ in_dom _ (fp a) m' = false /\ pf (fp a) = a.
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  tauto.  intros.  simpl in H0.
(* Goal: forall _ : @eq bool (N.odd (N.double a)) true, False *)
(* Goal: forall _ : @eq bool (N.odd (N.double a)) false, False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (option_sum _ (MapGet B m' a)).  intro y.  elim y; clear y; intros x y.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite y in H0.  left.  assumption.  intro y.  rewrite y in H0.
(* Goal: and (@eq bool (in_dom A (fp (pf a)) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp (pf a)) m') false) (@eq ad (pf (fp (pf a))) (pf a))) *)
(* Goal: forall _ : @In ad a1 l, or (@In ad a1 l) (and (@eq bool (in_dom A (fp a1) (M1 A a a0)) true) (and (@eq bool (in_dom B (fp a1) m') false) (@eq ad (pf (fp a1)) a1))) *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l m0 m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) m0) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a)))) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m m0) m')), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m m0)) true) (and (@eq bool (in_dom B (fp a) m') false) (@eq ad (pf (fp a)) a))) *)
  elim (in_inv H0).  intro H1.  right.  rewrite <- H1.  rewrite (H a).
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  unfold in_dom in |- *.  rewrite y.  simpl in |- *.  rewrite (Neqb_correct a).  split.
(* Goal: and (@eq bool match MapGet B m3 (N.div2 (fp a)) with | Some a => true | None => false end false) (@eq ad (pf (fp a)) a) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  reflexivity.  split.  reflexivity.  reflexivity.  tauto.  intro m0.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m'.  intros.  unfold MapDomRestrByApp1 in H2.
(* Goal: forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M0 A)) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad l *)
(* Goal: forall (a : ad) (a0 : A) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a1 : ad, @eq ad (fp (pf a1)) a1) (_ : forall (a1 : ad) (_ : @eq bool (in_dom A a1 (M1 A a a0)) true) (_ : @eq bool (in_dom B a1 m') false), not (@In ad (pf a1) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M1 A a a0) m') *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a m) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l m m')) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a m0) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l m0 m')) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m m0)) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m m0) m') *)
  elim (map_app_list1_lemma_2 _ _ _ _ H1 a H2).  tauto.  intro H3.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim H3; clear H3; intros.  right.  split.  assumption.  split.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  reflexivity.  assumption.  intros a a0 l pf fp H1 a1 H2.  unfold MapDomRestrByApp1 in H2.
(* Goal: forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M0 A)) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad l *)
(* Goal: forall (a : ad) (a0 : A) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a1 : ad, @eq ad (fp (pf a1)) a1) (_ : forall (a1 : ad) (_ : @eq bool (in_dom A a1 (M1 A a a0)) true) (_ : @eq bool (in_dom B a1 m') false), not (@In ad (pf a1) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M1 A a a0) m') *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a m) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l m m')) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a m0) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l m0 m')) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m m0)) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m m0) m') *)
  elim (map_app_list1_lemma_2 _ _ _ _ H1 a1 H2).  tauto.  intro H3.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim H3; clear H3; intros.  right.  unfold in_dom in H3.
(* Goal: and (@eq bool (in_dom A (fp a1) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a1) (M1 B a a0)) false) (@eq ad (pf (fp a1)) a1)) *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m) false) (@eq ad (pf (fp a)) a)))) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) m2) false) (@eq ad (pf (fp a)) a)))) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (a : ad) (_ : @In ad a (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2))), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m m2)) false) (@eq ad (pf (fp a)) a))) *)
  rewrite (MapRemove_semantics A (M2 A m0 m1) a (fp a1)) in H3.
(* Goal: forall _ : @eq bool (N.odd (N.double a)) true, False *)
(* Goal: forall _ : @eq bool (N.odd (N.double a)) false, False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Neqb a (fp a1))).  intro y.  rewrite y in H3.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  discriminate.  intro y.  rewrite y in H3.  split.  assumption.  split.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in |- *.  simpl in |- *.  rewrite y.  reflexivity.  assumption.  intros.
(* Goal: or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a))) *)
  simpl in H4.
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble a))) = a).
(* Goal: forall _ : forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a, no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble_plus_one a))) = a).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  elim
   (H0 m3 _ (fun a0 : ad => pf (Ndouble_plus_one a0))
      (fun a0 : ad => Ndiv2 (fp a0)) H5 _ H4).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro.  elim
   (H m2 _ (fun a0 : ad => pf (Ndouble a0))
      (fun a0 : ad => Ndiv2 (fp a0)) H6 _ H7).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  tauto.  intro.  elim H8; clear H8; intros.  elim H9; clear H9; intros.
(* Goal: or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a))) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  right.  elim (sumbool_of_bool (Nbit0 (fp a))).  intro y.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp a)) m1) true) (and (@eq bool (in_dom B (N.div2 (fp a)) m3) false) (@eq ad (pf (N.succ_double (N.div2 (fp a)))) a)), or (@In ad a l) (and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a))) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite <- H10 in y.  rewrite (H3 (Ndouble (Ndiv2 (fp a)))) in y.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_bit0 (Ndiv2 (fp a))) in y.  discriminate.  intro y.
(* Goal: @eq bool (in_dom B (N.double a) (M2 B m2 m3)) false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in |- *.  rewrite (MapGet_M2_bit_0_0 _ _ y m0 m1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (MapGet_M2_bit_0_0 _ _ y m2 m3).  split.  assumption.  split.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  rewrite (Ndiv2_double _ y) in H10.  assumption.  intro.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim H7; clear H7; intros.  elim H8; clear H8; intros.  right.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Nbit0 (fp a))).  intro y.  unfold in_dom in |- *.
(* Goal: and (@eq bool match MapGet A (M2 A m0 m1) (fp a) with | Some a => true | None => false end true) (and (@eq bool match MapGet B (M2 B m2 m3) (fp a) with | Some a => true | None => false end false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall _ : @eq bool (N.odd (fp a)) false, and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (MapGet_M2_bit_0_1 _ _ y m0 m1).  rewrite (MapGet_M2_bit_0_1 _ _ y m2 m3).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  split.  assumption.  split.  assumption.  rewrite (Ndiv2_double_plus_one _ y) in H9.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  intro y.  rewrite <- H9 in y.
(* Goal: and (@eq bool (in_dom A (fp a) (M2 A m0 m1)) true) (and (@eq bool (in_dom B (fp a) (M2 B m2 m3)) false) (@eq ad (pf (fp a)) a)) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (H3 (Ndouble_plus_one (Ndiv2 (fp a)))) in y.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_bit0 (Ndiv2 (fp a))) in y.  discriminate.  
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  rewrite (H3 (Ndouble_plus_one a0)).  apply Ndouble_plus_one_div2.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  rewrite (H3 (Ndouble a0)).  apply Ndouble_div2.
Qed.

Lemma MapDomRestrByApp1_lemma_4 :
 forall (m : Map A) (m' : Map B) (l : list ad) (pf fp : ad -> ad),
 (forall a : ad, fp (pf a) = a) ->
 (forall a : ad,
  in_dom _ a m = true -> in_dom _ a m' = false -> ~ In (pf a) l) ->
 no_dup_list _ l -> no_dup_list _ (MapDomRestrByApp1 pf l m m').
Proof.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  simple induction m.  simpl in |- *.  tauto.  intros.  unfold MapDomRestrByApp1 in |- *.
(* Goal: no_dup_list ad match MapGet B m' a with | Some b => l | None => @cons ad (pf a) l end *)
(* Goal: forall _ : @eq (option B) (MapGet B m' a) (@None B), no_dup_list ad match MapGet B m' a with | Some b0 => l | None => @cons ad (pf a) l end *)
(* Goal: forall (m : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a m) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l m m')) (m0 : Map A) (_ : forall (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a m0) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l m0 m')) (m' : Map B) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m m0)) true) (_ : @eq bool (in_dom B a m') false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m m0) m') *)
  elim (option_sum _ (MapGet _ m' a)).  intro y.  inversion y.  rewrite H2.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  intro y.  rewrite y.  apply no_dup_cons.  apply H0.  unfold in_dom in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  simpl in |- *.  rewrite (Neqb_correct a).  reflexivity.  unfold in_dom in |- *.  rewrite y.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  reflexivity.  assumption.  intro.  simple induction m'.  intros.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M1 B a a0)) *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  unfold MapDomRestrByApp1 in |- *.  apply map_app_list1_lemma_3 with (fp := fp).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  assumption.  intros.  apply H2.  assumption.  apply in_dom_M0.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  unfold MapDomRestrByApp1 in |- *.  apply map_app_list1_lemma_3 with (fp := fp).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  assumption.  intros.  apply H2.  unfold in_dom in |- *.
(* Goal: @eq bool (in_dom B a1 (M1 B a a0)) false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  unfold in_dom in H4.  rewrite (MapRemove_semantics A (M2 A m0 m1) a a1) in H4.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Neqb a a1)).  intro y.  rewrite y in H4.  discriminate.
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro y.  rewrite y in H4.  assumption.  unfold in_dom in H4.
(* Goal: @eq bool (in_dom B a1 (M1 B a a0)) false *)
(* Goal: forall (m : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m)) (m2 : Map B) (_ : forall (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a m2) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) m2)) (l : list ad) (pf fp : forall _ : ad, ad) (_ : forall a : ad, @eq ad (fp (pf a)) a) (_ : forall (a : ad) (_ : @eq bool (in_dom A a (M2 A m0 m1)) true) (_ : @eq bool (in_dom B a (M2 B m m2)) false), not (@In ad (pf a) l)) (_ : no_dup_list ad l), no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m m2)) *)
  rewrite (MapRemove_semantics A (M2 A m0 m1) a a1) in H4.
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim (sumbool_of_bool (Neqb a a1)).  intro y.  rewrite y in H4.  discriminate.
(* Goal: no_dup_list ad (MapDomRestrByApp1 pf l (M2 A m0 m1) (M2 B m2 m3)) *)
  intro y.  rewrite y in H4.  unfold in_dom in |- *.  simpl in |- *.  rewrite y.  reflexivity.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  simpl in |- *.
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble a))) = a).
(* Goal: forall _ : forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a, no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.succ_double a0)) (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) m1 m3) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  cut (forall a : ad, Ndiv2 (fp (pf (Ndouble_plus_one a))) = a).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intros.  apply H0 with (fp := fun a0 : ad => Ndiv2 (fp a0)).  intro.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (H3 (Ndouble_plus_one a)).  apply Ndouble_plus_one_div2.  intros.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold not in |- *.  intro.  elim
   (MapDomRestrByApp1_lemma_3 m0 m2 l (fun a0 : ad => pf (Ndouble a0))
      (fun a0 : ad => Ndiv2 (fp a0)) H7 (pf (Ndouble_plus_one a)) H10).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro.  unfold not in H4.  apply H4 with (a := Ndouble_plus_one a).
(* Goal: @eq bool (in_dom B (N.double a) (M2 B m2 m3)) false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in |- *.  rewrite (MapGet_M2_bit_0_1 _ _ (Ndouble_plus_one_bit0 a) m0 m1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_div2 a).  assumption.  unfold in_dom in |- *.
(* Goal: @eq bool match MapGet B (M2 B m2 m3) (N.succ_double a) with | Some a => true | None => false end false *)
(* Goal: @In ad (pf (N.succ_double a)) l *)
(* Goal: forall _ : and (@eq bool (in_dom A (N.div2 (fp (pf (N.succ_double a)))) m0) true) (and (@eq bool (in_dom B (N.div2 (fp (pf (N.succ_double a)))) m2) false) (@eq ad (pf (N.double (N.div2 (fp (pf (N.succ_double a)))))) (pf (N.succ_double a)))), False *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (MapGet_M2_bit_0_1 _ _ (Ndouble_plus_one_bit0 a) m2 m3).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_div2 a).  assumption.  assumption.  intros.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  elim H11; clear H11; intros.  elim H12; clear H12; intros.
(* Goal: False *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (H3 (Ndouble_plus_one a)) in H13.  rewrite (Ndouble_plus_one_div2 a) in H13.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  cut (Ndouble a = Ndouble_plus_one a).  intros.  elim (sumbool_of_bool (Nbit0 (Ndouble a))).
(* Goal: False *)
(* Goal: @eq N (N.double a) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  intro y.  rewrite (Ndouble_bit0 a) in y.  discriminate.  rewrite H14.
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_plus_one_bit0 a).  intro.  discriminate.  
(* Goal: @eq N (fp (pf (N.succ_double a))) (N.succ_double a) *)
(* Goal: no_dup_list ad (MapDomRestrByApp1 (fun a0 : ad => pf (N.double a0)) l m0 m2) *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite <- (H3 (Ndouble a)).  rewrite H13.  apply H3.  
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply H with (fp := fun a0 : ad => Ndiv2 (fp a0)).  assumption.  intros.  apply H4.
(* Goal: @eq bool (in_dom B (N.double a) (M2 B m2 m3)) false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  unfold in_dom in |- *.  rewrite (MapGet_M2_bit_0_0 _ _ (Ndouble_bit0 a) m0 m1).
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (Ndouble_div2 a).  assumption.  unfold in_dom in |- *.
(* Goal: @eq bool match MapGet B m2 (N.div2 (N.double a)) with | Some a => true | None => false end false *)
(* Goal: no_dup_list ad l *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  rewrite (MapGet_M2_bit_0_0 _ _ (Ndouble_bit0 a) m2 m3).  rewrite (Ndouble_div2 a).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.succ_double a)))) a *)
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  assumption.  assumption.  intros.  rewrite (H3 (Ndouble_plus_one a)).
(* Goal: forall a : ad, @eq N (N.div2 (fp (pf (N.double a)))) a *)
  apply Ndouble_plus_one_div2.  intro.  rewrite (H3 (Ndouble a)).
(* Goal: @eq N (N.div2 (N.double a)) a *)
  apply Ndouble_div2.
Qed.

End My_Map.