Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 705 insertions, 611 deletions

diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index e124a11f6b..fe598c4128 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -7,664 +7,758 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-Require Bool.
-Require Sumbool.
-Require Arith.
-Require ZArith.
-Require Addr.
-Require Adist.
-Require Addec.
-Require Map.
-Require Mapaxioms.
-Require Mapiter.
-Require Fset.
-Require Mapsubset.
-Require PolyList.
-Require Lsort.
-Require Peano_dec.
+Require Import Bool.
+Require Import Sumbool.
+Require Import Arith.
+Require Import ZArith.
+Require Import Addr.
+Require Import Adist.
+Require Import Addec.
+Require Import Map.
+Require Import Mapaxioms.
+Require Import Mapiter.
+Require Import Fset.
+Require Import Mapsubset.
+Require Import List.
+Require Import Lsort.
+Require Import Peano_dec.
 
 Section MapCard.
 
-  Variable A, B : Set.
+  Variables A B : Set.
+
+  Lemma MapCard_M0 : MapCard A (M0 A) = 0.
+  Proof.
+    trivial.
+  Qed.
+
+  Lemma MapCard_M1 : forall (a:ad) (y:A), MapCard A (M1 A a y) = 1.
+  Proof.
+    trivial.
+  Qed.
+
+  Lemma MapCard_is_O :
+   forall m:Map A, MapCard A m = 0 -> forall a:ad, MapGet A m a = NONE A.
+  Proof.
+    simple induction m. trivial.
+    intros a y H. discriminate H.
+    intros. simpl in H1. elim (plus_is_O _ _ H1). intros. rewrite (MapGet_M2_bit_0_if A m0 m1 a).
+    case (ad_bit_0 a). apply H0. assumption.
+    apply H. assumption.
+  Qed.
 
-  Lemma MapCard_M0 : (MapCard A (M0 A))=O.
+  Lemma MapCard_is_not_O :
+   forall (m:Map A) (a:ad) (y:A),
+     MapGet A m a = SOME A y -> {n : nat | MapCard A m = S n}.
   Proof.
-    Trivial.
+    simple induction m. intros. discriminate H.
+    intros a y a0 y0 H. simpl in H. elim (sumbool_of_bool (ad_eq a a0)). intro H0. split with 0.
+    reflexivity.
+    intro H0. rewrite H0 in H. discriminate H.
+    intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H2.
+    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. elim (H0 (ad_div_2 a) y H1). intros n H3.
+    simpl in |- *. rewrite H3. split with (MapCard A m0 + n).
+    rewrite <- (plus_Snm_nSm (MapCard A m0) n). reflexivity.
+    intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. elim (H (ad_div_2 a) y H1).
+    intros n H3. simpl in |- *. rewrite H3. split with (n + MapCard A m1). reflexivity.
   Qed.
 
-  Lemma MapCard_M1 : (a:ad) (y:A) (MapCard A (M1 A a y))=(1).
+  Lemma MapCard_is_one :
+   forall m:Map A,
+     MapCard A m = 1 -> {a : ad &  {y : A | MapGet A m a = SOME A y}}.
   Proof.
-    Trivial.
+    simple induction m. intro. discriminate H.
+    intros a y H. split with a. split with y. apply M1_semantics_1.
+    intros. simpl in H1. elim (plus_is_one (MapCard A m0) (MapCard A m1) H1).
+    intro H2. elim H2. intros. elim (H0 H4). intros a H5. split with (ad_double_plus_un a).
+    rewrite (MapGet_M2_bit_0_1 A _ (ad_double_plus_un_bit_0 a) m0 m1).
+    rewrite ad_double_plus_un_div_2. exact H5.
+    intro H2. elim H2. intros. elim (H H3). intros a H5. split with (ad_double a).
+    rewrite (MapGet_M2_bit_0_0 A _ (ad_double_bit_0 a) m0 m1).
+    rewrite ad_double_div_2. exact H5.
   Qed.
 
-  Lemma MapCard_is_O : (m:(Map A)) (MapCard A m)=O -> 
-      (a:ad) (MapGet A m a)=(NONE A).
+  Lemma MapCard_is_one_unique :
+   forall m:Map A,
+     MapCard A m = 1 ->
+     forall (a a':ad) (y y':A),
+       MapGet A m a = SOME A y ->
+       MapGet A m a' = SOME A y' -> a = a' /\ y = y'.
   Proof.
-    Induction m. Trivial.
-    Intros a y H. Discriminate H.
-    Intros. Simpl in H1. Elim (plus_is_O ? ? H1). Intros. Rewrite (MapGet_M2_bit_0_if A m0 m1 a).
-    Case (ad_bit_0 a). Apply H0. Assumption.
-    Apply H. Assumption.
+    simple induction m. intro. discriminate H.
+    intros. elim (sumbool_of_bool (ad_eq a a1)). intro H2. rewrite (ad_eq_complete _ _ H2) in H0.
+    rewrite (M1_semantics_1 A a1 a0) in H0. inversion H0. elim (sumbool_of_bool (ad_eq a a')).
+    intro H5. rewrite (ad_eq_complete _ _ H5) in H1. rewrite (M1_semantics_1 A a' a0) in H1.
+    inversion H1. rewrite <- (ad_eq_complete _ _ H2). rewrite <- (ad_eq_complete _ _ H5).
+    rewrite <- H4. rewrite <- H6. split; reflexivity.
+    intro H5. rewrite (M1_semantics_2 A a a' a0 H5) in H1. discriminate H1.
+    intro H2. rewrite (M1_semantics_2 A a a1 a0 H2) in H0. discriminate H0.
+    intros. simpl in H1. elim (plus_is_one _ _ H1). intro H4. elim H4. intros.
+    rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. elim (sumbool_of_bool (ad_bit_0 a)).
+    intro H7. rewrite H7 in H2. rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3.
+    elim (sumbool_of_bool (ad_bit_0 a')). intro H8. rewrite H8 in H3. elim (H0 H6 _ _ _ _ H2 H3).
+    intros. split. rewrite <- (ad_div_2_double_plus_un a H7).
+    rewrite <- (ad_div_2_double_plus_un a' H8). rewrite H9. reflexivity.
+    assumption.
+    intro H8. rewrite H8 in H3. rewrite (MapCard_is_O m0 H5 (ad_div_2 a')) in H3.
+    discriminate H3.
+    intro H7. rewrite H7 in H2. rewrite (MapCard_is_O m0 H5 (ad_div_2 a)) in H2.
+    discriminate H2.
+    intro H4. elim H4. intros. rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2.
+    elim (sumbool_of_bool (ad_bit_0 a)). intro H7. rewrite H7 in H2.
+    rewrite (MapCard_is_O m1 H6 (ad_div_2 a)) in H2. discriminate H2.
+    intro H7. rewrite H7 in H2. rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3.
+    elim (sumbool_of_bool (ad_bit_0 a')). intro H8. rewrite H8 in H3.
+    rewrite (MapCard_is_O m1 H6 (ad_div_2 a')) in H3. discriminate H3.
+    intro H8. rewrite H8 in H3. elim (H H5 _ _ _ _ H2 H3). intros. split.
+    rewrite <- (ad_div_2_double a H7). rewrite <- (ad_div_2_double a' H8).
+    rewrite H9. reflexivity.
+    assumption.
   Qed.
 
-  Lemma MapCard_is_not_O : (m:(Map A)) (a:ad) (y:A) (MapGet A m a)=(SOME A y) ->
-      {n:nat | (MapCard A m)=(S n)}.
+  Lemma length_as_fold :
+   forall (C:Set) (l:list C),
+     length l = fold_right (fun (_:C) (n:nat) => S n) 0 l.
   Proof.
-    Induction m. Intros. Discriminate H.
-    Intros a y a0 y0 H. Simpl in H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. Split with O.
-    Reflexivity.
-    Intro H0. Rewrite H0 in H. Discriminate H.
-    Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2.
-    Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. Elim (H0 (ad_div_2 a) y H1). Intros n H3.
-    Simpl. Rewrite H3. Split with (plus (MapCard A m0) n).
-    Rewrite <- (plus_Snm_nSm (MapCard A m0) n). Reflexivity.
-    Intro H2. Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. Elim (H (ad_div_2 a) y H1).
-    Intros n H3. Simpl. Rewrite H3. Split with (plus n (MapCard A m1)). Reflexivity.
+    simple induction l. reflexivity.
+    intros. simpl in |- *. rewrite H. reflexivity.
   Qed.
 
-  Lemma MapCard_is_one : (m:(Map A)) (MapCard A m)=(1) ->
-      {a:ad & {y:A | (MapGet A m a)=(SOME A y)}}.
-  Proof.
-    Induction m. Intro. Discriminate H.
-    Intros a y H. Split with a. Split with y. Apply M1_semantics_1.
-    Intros. Simpl in H1. Elim (plus_is_one (MapCard A m0) (MapCard A m1) H1).
-    Intro H2. Elim H2. Intros. Elim (H0 H4). Intros a H5. Split with (ad_double_plus_un a).
-    Rewrite (MapGet_M2_bit_0_1 A ? (ad_double_plus_un_bit_0 a) m0 m1).
-    Rewrite ad_double_plus_un_div_2. Exact H5.
-    Intro H2. Elim H2. Intros. Elim (H H3). Intros a H5. Split with (ad_double a).
-    Rewrite (MapGet_M2_bit_0_0 A ? (ad_double_bit_0 a) m0 m1).
-    Rewrite ad_double_div_2. Exact H5.
-  Qed.
-
-  Lemma MapCard_is_one_unique : (m:(Map A)) (MapCard A m)=(1) -> (a,a':ad) (y,y':A) 
-      (MapGet A m a)=(SOME A y) -> (MapGet A m a')=(SOME A y') ->
-        a=a' /\ y=y'.
-  Proof.
-    Induction m. Intro. Discriminate H.
-    Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2. Rewrite (ad_eq_complete ? ? H2) in H0.
-    Rewrite (M1_semantics_1 A a1 a0) in H0. Inversion H0. Elim (sumbool_of_bool (ad_eq a a')).
-    Intro H5. Rewrite (ad_eq_complete ? ? H5) in H1. Rewrite (M1_semantics_1 A a' a0) in H1.
-    Inversion H1. Rewrite <- (ad_eq_complete ? ? H2). Rewrite <- (ad_eq_complete ? ? H5).
-    Rewrite <- H4. Rewrite <- H6. (Split; Reflexivity).
-    Intro H5. Rewrite (M1_semantics_2 A a a' a0 H5) in H1. Discriminate H1.
-    Intro H2. Rewrite (M1_semantics_2 A a a1 a0 H2) in H0. Discriminate H0.
-    Intros. Simpl in H1. Elim (plus_is_one ? ? H1). Intro H4. Elim H4. Intros.
-    Rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. Elim (sumbool_of_bool (ad_bit_0 a)).
-    Intro H7. Rewrite H7 in H2. Rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3.
-    Elim (sumbool_of_bool (ad_bit_0 a')). Intro H8. Rewrite H8 in H3. Elim (H0 H6 ? ? ? ? H2 H3).
-    Intros. Split. Rewrite <- (ad_div_2_double_plus_un a H7).
-    Rewrite <- (ad_div_2_double_plus_un a' H8). Rewrite H9. Reflexivity.
-    Assumption.
-    Intro H8. Rewrite H8 in H3. Rewrite (MapCard_is_O m0 H5 (ad_div_2 a')) in H3.
-    Discriminate H3.
-    Intro H7. Rewrite H7 in H2. Rewrite (MapCard_is_O m0 H5 (ad_div_2 a)) in H2.
-    Discriminate H2.
-    Intro H4. Elim H4. Intros. Rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2.
-    Elim (sumbool_of_bool (ad_bit_0 a)). Intro H7. Rewrite H7 in H2.
-    Rewrite (MapCard_is_O m1 H6 (ad_div_2 a)) in H2. Discriminate H2.
-    Intro H7. Rewrite H7 in H2. Rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3.
-    Elim (sumbool_of_bool (ad_bit_0 a')). Intro H8. Rewrite H8 in H3.
-    Rewrite (MapCard_is_O m1 H6 (ad_div_2 a')) in H3. Discriminate H3.
-    Intro H8. Rewrite H8 in H3. Elim (H H5 ? ? ? ? H2 H3). Intros. Split.
-    Rewrite <- (ad_div_2_double a H7). Rewrite <- (ad_div_2_double a' H8).
-    Rewrite H9. Reflexivity.
-    Assumption.
-  Qed.
-
-  Lemma length_as_fold : (C:Set) (l:(list C)) 
-      (length l)=(fold_right [_:C][n:nat](S n) O l).
-  Proof.
-    Induction l. Reflexivity.
-    Intros. Simpl. Rewrite H. Reflexivity.
-  Qed.
-
-  Lemma length_as_fold_2 : (l:(alist A)) 
-      (length l)=(fold_right [r:ad*A][n:nat]let (a,y)=r in (plus (1) n) O l).
-  Proof.
-    Induction l. Reflexivity.
-    Intros. Simpl. Rewrite H. (Elim a; Reflexivity).
-  Qed.
-
-  Lemma MapCard_as_Fold_1 : (m:(Map A)) (pf:ad->ad)
-      (MapCard A m)=(MapFold1 A nat O plus [_:ad][_:A](1) pf m).
-  Proof.
-    Induction m. Trivial.
-    Trivial.
-    Intros. Simpl. Rewrite <- (H [a0:ad](pf (ad_double a0))).
-    Rewrite <- (H0 [a0:ad](pf (ad_double_plus_un a0))). Reflexivity.
-  Qed.
-
-  Lemma MapCard_as_Fold : 
-      (m:(Map A)) (MapCard A m)=(MapFold A nat O plus [_:ad][_:A](1) m).
-  Proof.
-    Intro. Exact (MapCard_as_Fold_1 m [a0:ad]a0).
+  Lemma length_as_fold_2 :
+   forall l:alist A,
+     length l =
+     fold_right (fun (r:ad * A) (n:nat) => let (a, y) := r in 1 + n) 0 l.
+  Proof.
+    simple induction l. reflexivity.
+    intros. simpl in |- *. rewrite H. elim a; reflexivity.
+  Qed.
+
+  Lemma MapCard_as_Fold_1 :
+   forall (m:Map A) (pf:ad -> ad),
+     MapCard A m = MapFold1 A nat 0 plus (fun (_:ad) (_:A) => 1) pf m.
+  Proof.
+    simple induction m. trivial.
+    trivial.
+    intros. simpl in |- *. rewrite <- (H (fun a0:ad => pf (ad_double a0))).
+    rewrite <- (H0 (fun a0:ad => pf (ad_double_plus_un a0))). reflexivity.
+  Qed.
+
+  Lemma MapCard_as_Fold :
+   forall m:Map A,
+     MapCard A m = MapFold A nat 0 plus (fun (_:ad) (_:A) => 1) m.
+  Proof.
+    intro. exact (MapCard_as_Fold_1 m (fun a0:ad => a0)).
   Qed.
  
-  Lemma MapCard_as_length : (m:(Map A)) (MapCard A m)=(length (alist_of_Map A m)).
-  Proof.
-    Intro. Rewrite MapCard_as_Fold. Rewrite length_as_fold_2.
-    Apply MapFold_as_fold with op:=plus neutral:=O f:=[_:ad][_:A](1). Exact plus_assoc_r.
-    Trivial.
-    Intro. Rewrite <- plus_n_O. Reflexivity.
-  Qed.
-
-  Lemma MapCard_Put1_equals_2 : (p:positive) (a,a':ad) (y,y':A)
-      (MapCard A (MapPut1 A a y a' y' p))=(2).
-  Proof.
-    Induction p. Intros. Simpl. (Case (ad_bit_0 a); Reflexivity).
-    Intros. Simpl. Case (ad_bit_0 a). Exact (H (ad_div_2 a) (ad_div_2 a') y y').
-    Simpl. Rewrite <- plus_n_O. Exact (H (ad_div_2 a) (ad_div_2 a') y y').
-    Intros. Simpl. (Case (ad_bit_0 a); Reflexivity).
-  Qed.
-
-  Lemma MapCard_Put_sum : (m,m':(Map A)) (a:ad) (y:A) (n,n':nat)
-      m'=(MapPut A m a y) -> n=(MapCard A m) -> n'=(MapCard A m') ->
-        {n'=n}+{n'=(S n)}.
-  Proof.
-    Induction m. Simpl. Intros. Rewrite H in H1. Simpl in H1. Right .
-    Rewrite H0. Rewrite H1. Reflexivity.
-    Intros a y m' a0 y0 n n' H H0 H1. Simpl in H. Elim (ad_sum (ad_xor a a0)). Intro H2.
-    Elim H2. Intros p H3. Rewrite H3 in H. Rewrite H in H1.
-    Rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H1. Simpl in H0. Right .
-    Rewrite H0. Rewrite H1. Reflexivity.
-    Intro H2. Rewrite H2 in H. Rewrite H in H1. Simpl in H1. Simpl in H0. Left .
-    Rewrite H0. Rewrite H1. Reflexivity.
-    Intros. Simpl in H2. Rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1.
-    Elim (sumbool_of_bool (ad_bit_0 a)). Intro H4. Rewrite H4 in H1.
-    Elim (H0 (MapPut A m1 (ad_div_2 a) y) (ad_div_2 a) y (MapCard A m1)
-       (MapCard A (MapPut A m1 (ad_div_2 a) y)) (refl_equal ? ?)
-       (refl_equal ? ?) (refl_equal ? ?)).
-    Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. Rewrite <- H2 in H3. Left .
-    Assumption.
-    Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3.
-    Rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H3.
-    Simpl in H3. Rewrite <- H2 in H3. Right . Assumption.
-    Intro H4. Rewrite H4 in H1.
-    Elim (H (MapPut A m0 (ad_div_2 a) y) (ad_div_2 a) y (MapCard A m0)
-       (MapCard A (MapPut A m0 (ad_div_2 a) y)) (refl_equal ? ?)
-       (refl_equal ? ?) (refl_equal ? ?)).
-    Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. Rewrite <- H2 in H3.
-    Left . Assumption.
-    Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. Simpl in H3. Rewrite <- H2 in H3.
-    Right . Assumption.
-  Qed.
-
-  Lemma MapCard_Put_lb : (m:(Map A)) (a:ad) (y:A)
-      (ge (MapCard A (MapPut A m a y)) (MapCard A m)).
-  Proof.
-    Unfold ge. Intros.
-    Elim (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m)
-       (MapCard A (MapPut A m a y)) (refl_equal ? ?) (refl_equal ? ?)
-       (refl_equal ? ?)).
-    Intro H. Rewrite H. Apply le_n.
-    Intro H. Rewrite H. Apply le_n_Sn.
-  Qed.
-
-  Lemma MapCard_Put_ub : (m:(Map A)) (a:ad) (y:A)
-      (le (MapCard A (MapPut A m a y)) (S (MapCard A m))).
-  Proof.
-    Intros.
-    Elim (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m)
-       (MapCard A (MapPut A m a y)) (refl_equal ? ?) (refl_equal ? ?)
-       (refl_equal ? ?)).
-    Intro H. Rewrite H. Apply le_n_Sn.
-    Intro H. Rewrite H. Apply le_n.
-  Qed.
-
-  Lemma MapCard_Put_1 : (m:(Map A)) (a:ad) (y:A)
-      (MapCard A (MapPut A m a y))=(MapCard A m) -> 
-        {y:A | (MapGet A m a)=(SOME A y)}.
-  Proof.
-    Induction m. Intros. Discriminate H.
-    Intros a y a0 y0 H. Simpl in H. Elim (ad_sum (ad_xor a a0)). Intro H0. Elim H0.
-    Intros p H1. Rewrite H1 in H. Rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H.
-    Discriminate H.
-    Intro H0. Rewrite H0 in H. Rewrite (ad_xor_eq ? ? H0). Split with y. Apply M1_semantics_1.
-    Intros. Rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. Elim (sumbool_of_bool (ad_bit_0 a)).
-    Intro H2. Rewrite H2 in H1. Simpl in H1. Elim (H0 (ad_div_2 a) y (simpl_plus_l ? ? ? H1)).
-    Intros y0 H3. Split with y0. Rewrite <- H3. Exact (MapGet_M2_bit_0_1 A a H2 m0 m1).
-    Intro H2. Rewrite H2 in H1. Simpl in H1.
-    Rewrite (plus_sym (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) in H1.
-    Rewrite (plus_sym (MapCard A m0) (MapCard A m1)) in H1.
-    Elim (H (ad_div_2 a) y (simpl_plus_l ? ? ? H1)). Intros y0 H3. Split with y0.
-    Rewrite <- H3. Exact (MapGet_M2_bit_0_0 A a H2 m0 m1).
-  Qed.
-
-  Lemma MapCard_Put_2 : (m:(Map A)) (a:ad) (y:A)
-      (MapCard A (MapPut A m a y))=(S (MapCard A m)) -> (MapGet A m a)=(NONE A).
-  Proof.
-    Induction m. Trivial.
-    Intros. Simpl in H. Elim (sumbool_of_bool (ad_eq a a1)). Intro H0.
-    Rewrite (ad_eq_complete ? ? H0) in H. Rewrite (ad_xor_nilpotent a1) in H. Discriminate H.
-    Intro H0. Exact (M1_semantics_2 A a a1 a0 H0).
-    Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2.
-    Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). Apply (H0 (ad_div_2 a) y).
-    Apply simpl_plus_l with n:=(MapCard A m0).
-    Rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)). Simpl in H1. Simpl. Rewrite <- H1.
-    Clear H1.
-    NewInduction a. Discriminate H2.
-    NewInduction p. Reflexivity.
-    Discriminate H2.
-    Reflexivity.
-    Intro H2. Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). Apply (H (ad_div_2 a) y).
-    Cut (plus (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1))
-         =(plus (S (MapCard A m0)) (MapCard A m1)).
-    Intro. Rewrite (plus_sym (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) in H3.
-    Rewrite (plus_sym (S (MapCard A m0)) (MapCard A m1)) in H3. Exact (simpl_plus_l ? ? ? H3).
-    Simpl. Simpl in H1. Rewrite <- H1. NewInduction a. Trivial.
-    NewInduction p. Discriminate H2.
-    Reflexivity.
-    Discriminate H2.
-  Qed.
-
-  Lemma MapCard_Put_1_conv : (m:(Map A)) (a:ad) (y,y':A)
-      (MapGet A m a)=(SOME A y) -> (MapCard A (MapPut A m a y'))=(MapCard A m).
-  Proof.
-    Intros.
-    Elim (MapCard_Put_sum m (MapPut A m a y') a y' (MapCard A m)
-           (MapCard A (MapPut A m a y')) (refl_equal ? ?) (refl_equal ? ?)
-           (refl_equal ? ?)).
-    Trivial.
-    Intro H0. Rewrite (MapCard_Put_2 m a y' H0) in H. Discriminate H.
-  Qed.
-
-  Lemma MapCard_Put_2_conv : (m:(Map A)) (a:ad) (y:A)
-      (MapGet A m a)=(NONE A) -> (MapCard A (MapPut A m a y))=(S (MapCard A m)).
-  Proof.
-    Intros.
-    Elim (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m)
-           (MapCard A (MapPut A m a y)) (refl_equal ? ?) (refl_equal ? ?)
-           (refl_equal ? ?)).
-    Intro H0. Elim (MapCard_Put_1 m a y H0). Intros y' H1. Rewrite H1 in H. Discriminate H.
-    Trivial.
-  Qed.
-
-  Lemma MapCard_ext : (m,m':(Map A))
-      (eqm A (MapGet A m) (MapGet A m')) -> (MapCard A m)=(MapCard A m').
-  Proof.
-    Unfold eqm. Intros. Rewrite (MapCard_as_length m). Rewrite (MapCard_as_length m').
-    Rewrite (alist_canonical A (alist_of_Map A m) (alist_of_Map A m')). Reflexivity.
-    Unfold eqm. Intro. Rewrite (Map_of_alist_semantics A (alist_of_Map A m) a).
-    Rewrite (Map_of_alist_semantics A (alist_of_Map A m') a). Rewrite (Map_of_alist_of_Map A m' a).
-    Rewrite (Map_of_alist_of_Map A m a). Exact (H a).
-    Apply alist_of_Map_sorts2.
-    Apply alist_of_Map_sorts2.
-  Qed.
-
-  Lemma MapCard_Dom : (m:(Map A)) (MapCard A m)=(MapCard unit (MapDom A m)).
-  Proof.
-    (Induction m; Trivial). Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity.
-  Qed.
-
-  Lemma MapCard_Dom_Put_behind : (m:(Map A)) (a:ad) (y:A)
-      (MapDom A (MapPut_behind A m a y))=(MapDom A (MapPut A m a y)).
-  Proof.
-    Induction m. Trivial.
-    Intros a y a0 y0. Simpl. Elim (ad_sum (ad_xor a a0)). Intro H. Elim H.
-    Intros p H0. Rewrite H0. Reflexivity.
-    Intro H. Rewrite H. Rewrite (ad_xor_eq ? ? H). Reflexivity.
-    Intros. Simpl. Elim (ad_sum a). Intro H1. Elim H1. Intros p H2. Rewrite H2. Case p.
-    Intro p0. Simpl. Rewrite H0. Reflexivity.
-    Intro p0. Simpl. Rewrite H. Reflexivity.
-    Simpl. Rewrite H0. Reflexivity.
-    Intro H1. Rewrite H1. Simpl. Rewrite H. Reflexivity.
-  Qed.
-
-  Lemma MapCard_Put_behind_Put : (m:(Map A)) (a:ad) (y:A)
-      (MapCard A (MapPut_behind A m a y))=(MapCard A (MapPut A m a y)).
-  Proof.
-    Intros. Rewrite MapCard_Dom. Rewrite MapCard_Dom. Rewrite MapCard_Dom_Put_behind.
-    Reflexivity.
-  Qed.
-
-  Lemma MapCard_Put_behind_sum : (m,m':(Map A)) (a:ad) (y:A) (n,n':nat)
-      m'=(MapPut_behind A m a y) -> n=(MapCard A m) -> n'=(MapCard A m') ->
-        {n'=n}+{n'=(S n)}.
-  Proof.
-    Intros. (Apply (MapCard_Put_sum m (MapPut A m a y) a y n n'); Trivial).
-    Rewrite <- MapCard_Put_behind_Put. Rewrite <- H. Assumption.
-  Qed.
+  Lemma MapCard_as_length :
+   forall m:Map A, MapCard A m = length (alist_of_Map A m).
+  Proof.
+    intro. rewrite MapCard_as_Fold. rewrite length_as_fold_2.
+    apply MapFold_as_fold with
+     (op := plus) (neutral := 0) (f := fun (_:ad) (_:A) => 1). exact plus_assoc_reverse.
+    trivial.
+    intro. rewrite <- plus_n_O. reflexivity.
+  Qed.
+
+  Lemma MapCard_Put1_equals_2 :
+   forall (p:positive) (a a':ad) (y y':A),
+     MapCard A (MapPut1 A a y a' y' p) = 2.
+  Proof.
+    simple induction p. intros. simpl in |- *. case (ad_bit_0 a); reflexivity.
+    intros. simpl in |- *. case (ad_bit_0 a). exact (H (ad_div_2 a) (ad_div_2 a') y y').
+    simpl in |- *. rewrite <- plus_n_O. exact (H (ad_div_2 a) (ad_div_2 a') y y').
+    intros. simpl in |- *. case (ad_bit_0 a); reflexivity.
+  Qed.
+
+  Lemma MapCard_Put_sum :
+   forall (m m':Map A) (a:ad) (y:A) (n n':nat),
+     m' = MapPut A m a y ->
+     n = MapCard A m -> n' = MapCard A m' -> {n' = n} + {n' = S n}.
+  Proof.
+    simple induction m. simpl in |- *. intros. rewrite H in H1. simpl in H1. right.
+    rewrite H0. rewrite H1. reflexivity.
+    intros a y m' a0 y0 n n' H H0 H1. simpl in H. elim (ad_sum (ad_xor a a0)). intro H2.
+    elim H2. intros p H3. rewrite H3 in H. rewrite H in H1.
+    rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H1. simpl in H0. right.
+    rewrite H0. rewrite H1. reflexivity.
+    intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. simpl in H0. left.
+    rewrite H0. rewrite H1. reflexivity.
+    intros. simpl in H2. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1.
+    elim (sumbool_of_bool (ad_bit_0 a)). intro H4. rewrite H4 in H1.
+    elim
+     (H0 (MapPut A m1 (ad_div_2 a) y) (ad_div_2 a) y (
+        MapCard A m1) (MapCard A (MapPut A m1 (ad_div_2 a) y)) (
+        refl_equal _) (refl_equal _) (refl_equal _)).
+    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3. left.
+    assumption.
+    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3.
+    rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H3.
+    simpl in H3. rewrite <- H2 in H3. right. assumption.
+    intro H4. rewrite H4 in H1.
+    elim
+     (H (MapPut A m0 (ad_div_2 a) y) (ad_div_2 a) y (
+        MapCard A m0) (MapCard A (MapPut A m0 (ad_div_2 a) y)) (
+        refl_equal _) (refl_equal _) (refl_equal _)).
+    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3.
+    left. assumption.
+    intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. simpl in H3. rewrite <- H2 in H3.
+    right. assumption.
+  Qed.
+
+  Lemma MapCard_Put_lb :
+   forall (m:Map A) (a:ad) (y:A), MapCard A (MapPut A m a y) >= MapCard A m.
+  Proof.
+    unfold ge in |- *. intros.
+    elim
+     (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m)
+        (MapCard A (MapPut A m a y)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H. rewrite H. apply le_n.
+    intro H. rewrite H. apply le_n_Sn.
+  Qed.
+
+  Lemma MapCard_Put_ub :
+   forall (m:Map A) (a:ad) (y:A),
+     MapCard A (MapPut A m a y) <= S (MapCard A m).
+  Proof.
+    intros.
+    elim
+     (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m)
+        (MapCard A (MapPut A m a y)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H. rewrite H. apply le_n_Sn.
+    intro H. rewrite H. apply le_n.
+  Qed.
+
+  Lemma MapCard_Put_1 :
+   forall (m:Map A) (a:ad) (y:A),
+     MapCard A (MapPut A m a y) = MapCard A m ->
+     {y : A | MapGet A m a = SOME A y}.
+  Proof.
+    simple induction m. intros. discriminate H.
+    intros a y a0 y0 H. simpl in H. elim (ad_sum (ad_xor a a0)). intro H0. elim H0.
+    intros p H1. rewrite H1 in H. rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H.
+    discriminate H.
+    intro H0. rewrite H0 in H. rewrite (ad_xor_eq _ _ H0). split with y. apply M1_semantics_1.
+    intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. elim (sumbool_of_bool (ad_bit_0 a)).
+    intro H2. rewrite H2 in H1. simpl in H1. elim (H0 (ad_div_2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)).
+    intros y0 H3. split with y0. rewrite <- H3. exact (MapGet_M2_bit_0_1 A a H2 m0 m1).
+    intro H2. rewrite H2 in H1. simpl in H1.
+    rewrite
+     (plus_comm (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1))
+      in H1.
+    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1.
+    elim (H (ad_div_2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). intros y0 H3. split with y0.
+    rewrite <- H3. exact (MapGet_M2_bit_0_0 A a H2 m0 m1).
+  Qed.
+
+  Lemma MapCard_Put_2 :
+   forall (m:Map A) (a:ad) (y:A),
+     MapCard A (MapPut A m a y) = S (MapCard A m) -> MapGet A m a = NONE A.
+  Proof.
+    simple induction m. trivial.
+    intros. simpl in H. elim (sumbool_of_bool (ad_eq a a1)). intro H0.
+    rewrite (ad_eq_complete _ _ H0) in H. rewrite (ad_xor_nilpotent a1) in H. discriminate H.
+    intro H0. exact (M1_semantics_2 A a a1 a0 H0).
+    intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H2.
+    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply (H0 (ad_div_2 a) y).
+    apply (fun n m p:nat => plus_reg_l m p n) with (n := MapCard A m0).
+    rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)). simpl in H1. simpl in |- *. rewrite <- H1.
+    clear H1.
+    induction a. discriminate H2.
+    induction p. reflexivity.
+    discriminate H2.
+    reflexivity.
+    intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply (H (ad_div_2 a) y).
+    cut
+     (MapCard A (MapPut A m0 (ad_div_2 a) y) + MapCard A m1 =
+      S (MapCard A m0) + MapCard A m1).
+    intro. rewrite (plus_comm (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1))
+   in H3.
+    rewrite (plus_comm (S (MapCard A m0)) (MapCard A m1)) in H3. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H3).
+    simpl in |- *. simpl in H1. rewrite <- H1. induction a. trivial.
+    induction p. discriminate H2.
+    reflexivity.
+    discriminate H2.
+  Qed.
+
+  Lemma MapCard_Put_1_conv :
+   forall (m:Map A) (a:ad) (y y':A),
+     MapGet A m a = SOME A y -> MapCard A (MapPut A m a y') = MapCard A m.
+  Proof.
+    intros.
+    elim
+     (MapCard_Put_sum m (MapPut A m a y') a y' (MapCard A m)
+        (MapCard A (MapPut A m a y')) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    trivial.
+    intro H0. rewrite (MapCard_Put_2 m a y' H0) in H. discriminate H.
+  Qed.
+
+  Lemma MapCard_Put_2_conv :
+   forall (m:Map A) (a:ad) (y:A),
+     MapGet A m a = NONE A -> MapCard A (MapPut A m a y) = S (MapCard A m).
+  Proof.
+    intros.
+    elim
+     (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m)
+        (MapCard A (MapPut A m a y)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H0. elim (MapCard_Put_1 m a y H0). intros y' H1. rewrite H1 in H. discriminate H.
+    trivial.
+  Qed.
+
+  Lemma MapCard_ext :
+   forall m m':Map A,
+     eqm A (MapGet A m) (MapGet A m') -> MapCard A m = MapCard A m'.
+  Proof.
+    unfold eqm in |- *. intros. rewrite (MapCard_as_length m). rewrite (MapCard_as_length m').
+    rewrite (alist_canonical A (alist_of_Map A m) (alist_of_Map A m')). reflexivity.
+    unfold eqm in |- *. intro. rewrite (Map_of_alist_semantics A (alist_of_Map A m) a).
+    rewrite (Map_of_alist_semantics A (alist_of_Map A m') a). rewrite (Map_of_alist_of_Map A m' a).
+    rewrite (Map_of_alist_of_Map A m a). exact (H a).
+    apply alist_of_Map_sorts2.
+    apply alist_of_Map_sorts2.
+  Qed.
+
+  Lemma MapCard_Dom : forall m:Map A, MapCard A m = MapCard unit (MapDom A m).
+  Proof.
+    simple induction m; trivial. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity.
+  Qed.
+
+  Lemma MapCard_Dom_Put_behind :
+   forall (m:Map A) (a:ad) (y:A),
+     MapDom A (MapPut_behind A m a y) = MapDom A (MapPut A m a y).
+  Proof.
+    simple induction m. trivial.
+    intros a y a0 y0. simpl in |- *. elim (ad_sum (ad_xor a a0)). intro H. elim H.
+    intros p H0. rewrite H0. reflexivity.
+    intro H. rewrite H. rewrite (ad_xor_eq _ _ H). reflexivity.
+    intros. simpl in |- *. elim (ad_sum a). intro H1. elim H1. intros p H2. rewrite H2. case p.
+    intro p0. simpl in |- *. rewrite H0. reflexivity.
+    intro p0. simpl in |- *. rewrite H. reflexivity.
+    simpl in |- *. rewrite H0. reflexivity.
+    intro H1. rewrite H1. simpl in |- *. rewrite H. reflexivity.
+  Qed.
+
+  Lemma MapCard_Put_behind_Put :
+   forall (m:Map A) (a:ad) (y:A),
+     MapCard A (MapPut_behind A m a y) = MapCard A (MapPut A m a y).
+  Proof.
+    intros. rewrite MapCard_Dom. rewrite MapCard_Dom. rewrite MapCard_Dom_Put_behind.
+    reflexivity.
+  Qed.
 
-  Lemma MapCard_makeM2 : (m,m':(Map A))
-      (MapCard A (makeM2 A m m'))=(plus (MapCard A m) (MapCard A m')).
+  Lemma MapCard_Put_behind_sum :
+   forall (m m':Map A) (a:ad) (y:A) (n n':nat),
+     m' = MapPut_behind A m a y ->
+     n = MapCard A m -> n' = MapCard A m' -> {n' = n} + {n' = S n}.
+  Proof.
+    intros. apply (MapCard_Put_sum m (MapPut A m a y) a y n n'); trivial.
+    rewrite <- MapCard_Put_behind_Put. rewrite <- H. assumption.
+  Qed.
+
+  Lemma MapCard_makeM2 :
+   forall m m':Map A, MapCard A (makeM2 A m m') = MapCard A m + MapCard A m'.
   Proof.
-    Intros. Rewrite (MapCard_ext ? ? (makeM2_M2 A m m')). Reflexivity.
+    intros. rewrite (MapCard_ext _ _ (makeM2_M2 A m m')). reflexivity.
   Qed.
  
-  Lemma MapCard_Remove_sum : (m,m':(Map A)) (a:ad) (n,n':nat)
-      m'=(MapRemove A m a) -> n=(MapCard A m) -> n'=(MapCard A m') ->
-        {n=n'}+{n=(S n')}.
-  Proof.
-    Induction m. Simpl. Intros. Rewrite H in H1. Simpl in H1. Left . Rewrite H1. Assumption.
-    Simpl. Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2. Rewrite H2 in H.
-    Rewrite H in H1. Simpl in H1. Right . Rewrite H1. Assumption.
-    Intro H2. Rewrite H2 in H. Rewrite H in H1. Simpl in H1. Left . Rewrite H1. Assumption.
-    Intros. Simpl in H1. Simpl in H2. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H4.
-    Rewrite H4 in H1. Rewrite H1 in H3.
-    Rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H3.
-    Elim (H0 (MapRemove A m1 (ad_div_2 a)) (ad_div_2 a) (MapCard A m1)
-             (MapCard A (MapRemove A m1 (ad_div_2 a))) (refl_equal ? ?)
-             (refl_equal ? ?) (refl_equal ? ?)).
-    Intro H5. Rewrite H5 in H2. Left . Rewrite H3. Exact H2.
-    Intro H5. Rewrite H5 in H2.
-    Rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a)))) in H2.
-    Right . Rewrite H3. Exact H2.
-    Intro H4. Rewrite H4 in H1. Rewrite H1 in H3.
-    Rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H3.
-    Elim (H (MapRemove A m0 (ad_div_2 a)) (ad_div_2 a) (MapCard A m0)
-            (MapCard A (MapRemove A m0 (ad_div_2 a))) (refl_equal ? ?)
-            (refl_equal ? ?) (refl_equal ? ?)).
-    Intro H5. Rewrite H5 in H2. Left . Rewrite H3. Exact H2.
-    Intro H5. Rewrite H5 in H2. Right . Rewrite H3. Exact H2.
-  Qed.
-
-  Lemma MapCard_Remove_ub : (m:(Map A)) (a:ad)
-      (le (MapCard A (MapRemove A m a)) (MapCard A m)).
-  Proof.
-    Intros.
-    Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
-           (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?)
-           (refl_equal ? ?)).
-    Intro H. Rewrite H. Apply le_n.
-    Intro H. Rewrite H. Apply le_n_Sn.
-  Qed.
-
-  Lemma MapCard_Remove_lb : (m:(Map A)) (a:ad)
-      (ge (S (MapCard A (MapRemove A m a))) (MapCard A m)).
-  Proof.
-    Unfold ge. Intros.
-    Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
-           (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?)
-           (refl_equal ? ?)).
-    Intro H. Rewrite H. Apply le_n_Sn.
-    Intro H. Rewrite H. Apply le_n.
-  Qed.
-
-  Lemma MapCard_Remove_1 : (m:(Map A)) (a:ad)
-      (MapCard A (MapRemove A m a))=(MapCard A m) -> (MapGet A m a)=(NONE A).
-  Proof.
-    Induction m. Trivial.
-    Simpl. Intros a y a0 H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0.
-    Rewrite H0 in H. Discriminate H.
-    Intro H0. Rewrite H0. Reflexivity.
-    Intros. Simpl in H1. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. Rewrite H2 in H1.
-    Rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1.
-    Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). Apply H0. Exact (simpl_plus_l ? ? ? H1).
-    Intro H2. Rewrite H2 in H1.
-    Rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1.
-    Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). Apply H.
-    Rewrite (plus_sym (MapCard A (MapRemove A m0 (ad_div_2 a))) (MapCard A m1)) in H1.
-    Rewrite (plus_sym (MapCard A m0) (MapCard A m1)) in H1. Exact (simpl_plus_l ? ? ? H1).
-  Qed.
-
-  Lemma MapCard_Remove_2 : (m:(Map A)) (a:ad)
-      (S (MapCard A (MapRemove A m a)))=(MapCard A m) -> 
-        {y:A | (MapGet A m a)=(SOME A y)}.
-  Proof.
-    Induction m. Intros. Discriminate H.
-    Intros a y a0 H. Simpl in H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0.
-    Rewrite (ad_eq_complete ? ? H0). Split with y. Exact (M1_semantics_1 A a0 y).
-    Intro H0. Rewrite H0 in H. Discriminate H.
-    Intros. Simpl in H1. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. Rewrite H2 in H1.
-    Rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1.
-    Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). Apply H0.
-    Change (plus (S (MapCard A m0)) (MapCard A (MapRemove A m1 (ad_div_2 a))))
-            =(plus (MapCard A m0) (MapCard A m1)) in H1.
-    Rewrite (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a)))) in H1.
-    Exact (simpl_plus_l ? ? ? H1).
-    Intro H2. Rewrite H2 in H1. Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). Apply H.
-    Rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1.
-    Change (plus (S (MapCard A (MapRemove A m0 (ad_div_2 a)))) (MapCard A m1))
-      	   =(plus (MapCard A m0) (MapCard A m1)) in H1.
-    Rewrite (plus_sym (S (MapCard A (MapRemove A m0 (ad_div_2 a)))) (MapCard A m1)) in H1.
-    Rewrite (plus_sym (MapCard A m0) (MapCard A m1)) in H1. Exact (simpl_plus_l ? ? ? H1).
-  Qed.
-
-  Lemma MapCard_Remove_1_conv : (m:(Map A)) (a:ad)
-      (MapGet A m a)=(NONE A) -> (MapCard A (MapRemove A m a))=(MapCard A m).
-  Proof.
-    Intros.
-    Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
-           (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?)
-           (refl_equal ? ?)).
-    Intro H0. Rewrite H0. Reflexivity.
-    Intro H0. Elim (MapCard_Remove_2 m a (sym_eq ? ? ? H0)). Intros y H1. Rewrite H1 in H.
-    Discriminate H.
-  Qed.
-
-  Lemma MapCard_Remove_2_conv : (m:(Map A)) (a:ad) (y:A)
-      (MapGet A m a)=(SOME A y) -> 
-        (S (MapCard A (MapRemove A m a)))=(MapCard A m).
-  Proof.
-    Intros.
-    Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
-           (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?)
-           (refl_equal ? ?)).
-    Intro H0. Rewrite (MapCard_Remove_1 m a (sym_eq ? ? ? H0)) in H. Discriminate H.
-    Intro H0. Rewrite H0. Reflexivity.
-  Qed.
-
-  Lemma MapMerge_Restr_Card : (m,m':(Map A))
-      (plus (MapCard A m) (MapCard A m'))=
-      (plus (MapCard A (MapMerge A m m')) (MapCard A (MapDomRestrTo A A m m'))).
-  Proof.
-    Induction m. Simpl. Intro. Apply plus_n_O.
-    Simpl. Intros a y m'. Elim (option_sum A (MapGet A m' a)). Intro H. Elim H. Intros y0 H0.
-    Rewrite H0. Rewrite MapCard_Put_behind_Put. Rewrite (MapCard_Put_1_conv m' a y0 y H0).
-    Simpl. Rewrite <- plus_Snm_nSm. Apply plus_n_O.
-    Intro H. Rewrite H. Rewrite MapCard_Put_behind_Put. Rewrite (MapCard_Put_2_conv m' a y H).
-    Apply plus_n_O.
-    Intros.
-    Change (plus (plus (MapCard A m0) (MapCard A m1)) (MapCard A m'))
-            =(plus (MapCard A (MapMerge A (M2 A m0 m1) m'))
-               (MapCard A (MapDomRestrTo A A (M2 A m0 m1) m'))).
-    Elim m'. Reflexivity.
-    Intros a y. Unfold MapMerge. Unfold MapDomRestrTo.
-    Elim (option_sum A (MapGet A (M2 A m0 m1) a)). Intro H1. Elim H1. Intros y0 H2. Rewrite H2.
-    Rewrite (MapCard_Put_1_conv (M2 A m0 m1) a y0 y H2). Reflexivity.
-    Intro H1. Rewrite H1. Rewrite (MapCard_Put_2_conv (M2 A m0 m1) a y H1). Simpl.
-    Rewrite <- (plus_Snm_nSm (plus (MapCard A m0) (MapCard A m1)) O). Reflexivity.
-    Intros. Simpl.
-    Rewrite (plus_permute_2_in_4 (MapCard A m0) (MapCard A m1) (MapCard A m2) (MapCard A m3)).
-    Rewrite (H m2). Rewrite (H0 m3).
-    Rewrite (MapCard_makeM2 (MapDomRestrTo A A m0 m2) (MapDomRestrTo A A m1 m3)).
-    Apply plus_permute_2_in_4.
-  Qed.
-
-  Lemma MapMerge_disjoint_Card : (m,m':(Map A)) (MapDisjoint A A m m') ->
-      	(MapCard A (MapMerge A m m'))=(plus (MapCard A m) (MapCard A m')).
-  Proof.
-    Intros. Rewrite (MapMerge_Restr_Card m m').
-    Rewrite (MapCard_ext ? ? (MapDisjoint_imp_2 ? ? ? ? H)). Apply plus_n_O.
-  Qed.
-
-  Lemma MapSplit_Card : (m:(Map A)) (m':(Map B))
-      (MapCard A m)=(plus (MapCard A (MapDomRestrTo A B m m'))
-                          (MapCard A (MapDomRestrBy A B m m'))).
-  Proof.
-    Intros. Rewrite (MapCard_ext ? ? (MapDom_Split_1 A B m m')). Apply MapMerge_disjoint_Card.
-    Apply MapDisjoint_2_imp. Unfold MapDisjoint_2. Apply MapDom_Split_3.
-  Qed.
-
-  Lemma MapMerge_Card_ub : (m,m':(Map A))
-      (le (MapCard A (MapMerge A m m')) (plus (MapCard A m) (MapCard A m'))).
-  Proof.
-    Intros. Rewrite MapMerge_Restr_Card. Apply le_plus_l.
-  Qed.
-
-  Lemma MapDomRestrTo_Card_ub_l : (m:(Map A)) (m':(Map B))
-      (le (MapCard A (MapDomRestrTo A B m m')) (MapCard A m)).
-  Proof.
-    Intros. Rewrite (MapSplit_Card m m'). Apply le_plus_l.
-  Qed.
-
-  Lemma MapDomRestrBy_Card_ub_l : (m:(Map A)) (m':(Map B))
-      (le (MapCard A (MapDomRestrBy A B m m')) (MapCard A m)).
-  Proof.
-    Intros. Rewrite (MapSplit_Card m m'). Apply le_plus_r.
-  Qed.
-
-  Lemma MapMerge_Card_disjoint : (m,m':(Map A))
-      (MapCard A (MapMerge A m m'))=(plus (MapCard A m) (MapCard A m')) ->
-        (MapDisjoint A A m m').
-  Proof.
-    Induction m. Intros. Apply Map_M0_disjoint.
-    Simpl. Intros. Rewrite (MapCard_Put_behind_Put m' a a0) in H. Unfold MapDisjoint in_dom.
-    Simpl. Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2.
-    Rewrite (ad_eq_complete ? ? H2) in H. Rewrite (MapCard_Put_2 m' a1 a0 H) in H1.
-    Discriminate H1.
-    Intro H2. Rewrite H2 in H0. Discriminate H0.
-    Induction m'. Intros. Apply Map_disjoint_M0.
-    Intros a y H1. Rewrite <- (MapCard_ext ? ? (MapPut_as_Merge A (M2 A m0 m1) a y)) in H1.
-    Unfold 3 MapCard in H1. Rewrite <- (plus_Snm_nSm (MapCard A (M2 A m0 m1)) O) in H1.
-    Rewrite <- (plus_n_O (S (MapCard A (M2 A m0 m1)))) in H1. Unfold MapDisjoint in_dom.
-    Unfold 2 MapGet. Intros. Elim (sumbool_of_bool (ad_eq a a0)). Intro H4.
-    Rewrite <- (ad_eq_complete ? ? H4) in H2. Rewrite (MapCard_Put_2 ? ? ? H1) in H2.
-    Discriminate H2.
-    Intro H4. Rewrite H4 in H3. Discriminate H3.
-    Intros. Unfold MapDisjoint. Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H6.
-    Unfold MapDisjoint in H0. Apply H0 with m':=m3 a:=(ad_div_2 a). Apply le_antisym.
-    Apply MapMerge_Card_ub.
-    Apply simpl_le_plus_l with p:=(plus (MapCard A m0) (MapCard A m2)).
-    Rewrite (plus_permute_2_in_4 (MapCard A m0) (MapCard A m2) (MapCard A m1) (MapCard A m3)).
-    Change (MapCard A (M2 A (MapMerge A m0 m2) (MapMerge A m1 m3)))
-           =(plus (plus (MapCard A m0) (MapCard A m1)) (plus (MapCard A m2) (MapCard A m3))) in H3.
-    Rewrite <- H3. Simpl. Apply le_reg_r. Apply MapMerge_Card_ub.
-    Elim (in_dom_some ? ? ? H4). Intros y H7. Rewrite (MapGet_M2_bit_0_1 ? a H6 m0 m1) in H7.
-    Unfold in_dom. Rewrite H7. Reflexivity.
-    Elim (in_dom_some ? ? ? H5). Intros y H7. Rewrite (MapGet_M2_bit_0_1 ? a H6 m2 m3) in H7.
-    Unfold in_dom. Rewrite H7. Reflexivity.
-    Intro H6. Unfold MapDisjoint in H. Apply H with m':=m2 a:=(ad_div_2 a). Apply le_antisym.
-    Apply MapMerge_Card_ub.
-    Apply simpl_le_plus_l with p:=(plus (MapCard A m1) (MapCard A m3)).
-    Rewrite (plus_sym (plus (MapCard A m1) (MapCard A m3)) (plus (MapCard A m0) (MapCard A m2))).
-    Rewrite (plus_permute_2_in_4 (MapCard A m0) (MapCard A m2) (MapCard A m1) (MapCard A m3)).
-    Rewrite (plus_sym (plus (MapCard A m1) (MapCard A m3)) (MapCard A (MapMerge A m0 m2))).
-    Change (plus (MapCard A (MapMerge A m0 m2)) (MapCard A (MapMerge A m1 m3)))
-           =(plus (plus (MapCard A m0) (MapCard A m1)) (plus (MapCard A m2) (MapCard A m3))) in H3.
-    Rewrite <- H3. Apply le_reg_l. Apply MapMerge_Card_ub.
-    Elim (in_dom_some ? ? ? H4). Intros y H7. Rewrite (MapGet_M2_bit_0_0 ? a H6 m0 m1) in H7.
-    Unfold in_dom. Rewrite H7. Reflexivity.
-    Elim (in_dom_some ? ? ? H5). Intros y H7. Rewrite (MapGet_M2_bit_0_0 ? a H6 m2 m3) in H7.
-    Unfold in_dom. Rewrite H7. Reflexivity.
-  Qed.
-
-  Lemma MapCard_is_Sn : (m:(Map A)) (n:nat) (MapCard ? m)=(S n) -> 
-      {a:ad | (in_dom ? a m)=true}.
-  Proof.
-    Induction m. Intros. Discriminate H.
-    Intros a y n H. Split with a. Unfold in_dom. Rewrite (M1_semantics_1 ? a y). Reflexivity.
-    Intros. Simpl in H1. Elim (O_or_S (MapCard ? m0)). Intro H2. Elim H2. Intros m2 H3.
-    Elim (H ? (sym_eq ? ? ? H3)). Intros a H4. Split with (ad_double a). Unfold in_dom.
-    Rewrite (MapGet_M2_bit_0_0 A (ad_double a) (ad_double_bit_0 a) m0 m1).
-    Rewrite (ad_double_div_2 a). Elim (in_dom_some ? ? ? H4). Intros y H5. Rewrite H5. Reflexivity.
-    Intro H2. Rewrite <- H2 in H1. Simpl in H1. Elim (H0 ? H1). Intros a H3.
-    Split with (ad_double_plus_un a). Unfold in_dom.
-    Rewrite (MapGet_M2_bit_0_1 A (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) m0 m1).
-    Rewrite (ad_double_plus_un_div_2 a). Elim (in_dom_some ? ? ? H3). Intros y H4. Rewrite H4.
-    Reflexivity.
+  Lemma MapCard_Remove_sum :
+   forall (m m':Map A) (a:ad) (n n':nat),
+     m' = MapRemove A m a ->
+     n = MapCard A m -> n' = MapCard A m' -> {n = n'} + {n = S n'}.
+  Proof.
+    simple induction m. simpl in |- *. intros. rewrite H in H1. simpl in H1. left. rewrite H1. assumption.
+    simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H2. rewrite H2 in H.
+    rewrite H in H1. simpl in H1. right. rewrite H1. assumption.
+    intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. left. rewrite H1. assumption.
+    intros. simpl in H1. simpl in H2. elim (sumbool_of_bool (ad_bit_0 a)). intro H4.
+    rewrite H4 in H1. rewrite H1 in H3.
+    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H3.
+    elim
+     (H0 (MapRemove A m1 (ad_div_2 a)) (ad_div_2 a) (
+        MapCard A m1) (MapCard A (MapRemove A m1 (ad_div_2 a)))
+        (refl_equal _) (refl_equal _) (refl_equal _)).
+    intro H5. rewrite H5 in H2. left. rewrite H3. exact H2.
+    intro H5. rewrite H5 in H2.
+    rewrite <-
+     (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a))))
+      in H2.
+    right. rewrite H3. exact H2.
+    intro H4. rewrite H4 in H1. rewrite H1 in H3.
+    rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H3.
+    elim
+     (H (MapRemove A m0 (ad_div_2 a)) (ad_div_2 a) (
+        MapCard A m0) (MapCard A (MapRemove A m0 (ad_div_2 a)))
+        (refl_equal _) (refl_equal _) (refl_equal _)).
+    intro H5. rewrite H5 in H2. left. rewrite H3. exact H2.
+    intro H5. rewrite H5 in H2. right. rewrite H3. exact H2.
+  Qed.
+
+  Lemma MapCard_Remove_ub :
+   forall (m:Map A) (a:ad), MapCard A (MapRemove A m a) <= MapCard A m.
+  Proof.
+    intros.
+    elim
+     (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
+        (MapCard A (MapRemove A m a)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H. rewrite H. apply le_n.
+    intro H. rewrite H. apply le_n_Sn.
+  Qed.
+
+  Lemma MapCard_Remove_lb :
+   forall (m:Map A) (a:ad), S (MapCard A (MapRemove A m a)) >= MapCard A m.
+  Proof.
+    unfold ge in |- *. intros.
+    elim
+     (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
+        (MapCard A (MapRemove A m a)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H. rewrite H. apply le_n_Sn.
+    intro H. rewrite H. apply le_n.
+  Qed.
+
+  Lemma MapCard_Remove_1 :
+   forall (m:Map A) (a:ad),
+     MapCard A (MapRemove A m a) = MapCard A m -> MapGet A m a = NONE A.
+  Proof.
+    simple induction m. trivial.
+    simpl in |- *. intros a y a0 H. elim (sumbool_of_bool (ad_eq a a0)). intro H0.
+    rewrite H0 in H. discriminate H.
+    intro H0. rewrite H0. reflexivity.
+    intros. simpl in H1. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. rewrite H2 in H1.
+    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1.
+    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply H0. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1).
+    intro H2. rewrite H2 in H1.
+    rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1.
+    rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply H.
+    rewrite
+     (plus_comm (MapCard A (MapRemove A m0 (ad_div_2 a))) (MapCard A m1))
+      in H1.
+    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1).
+  Qed.
+
+  Lemma MapCard_Remove_2 :
+   forall (m:Map A) (a:ad),
+     S (MapCard A (MapRemove A m a)) = MapCard A m ->
+     {y : A | MapGet A m a = SOME A y}.
+  Proof.
+    simple induction m. intros. discriminate H.
+    intros a y a0 H. simpl in H. elim (sumbool_of_bool (ad_eq a a0)). intro H0.
+    rewrite (ad_eq_complete _ _ H0). split with y. exact (M1_semantics_1 A a0 y).
+    intro H0. rewrite H0 in H. discriminate H.
+    intros. simpl in H1. elim (sumbool_of_bool (ad_bit_0 a)). intro H2. rewrite H2 in H1.
+    rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1.
+    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply H0.
+    change
+      (S (MapCard A m0) + MapCard A (MapRemove A m1 (ad_div_2 a)) =
+       MapCard A m0 + MapCard A m1) in H1.
+    rewrite
+     (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a))))
+      in H1.
+    exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1).
+    intro H2. rewrite H2 in H1. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply H.
+    rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1.
+    change
+      (S (MapCard A (MapRemove A m0 (ad_div_2 a))) + MapCard A m1 =
+       MapCard A m0 + MapCard A m1) in H1.
+    rewrite
+     (plus_comm (S (MapCard A (MapRemove A m0 (ad_div_2 a)))) (MapCard A m1))
+      in H1.
+    rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1).
+  Qed.
+
+  Lemma MapCard_Remove_1_conv :
+   forall (m:Map A) (a:ad),
+     MapGet A m a = NONE A -> MapCard A (MapRemove A m a) = MapCard A m.
+  Proof.
+    intros.
+    elim
+     (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
+        (MapCard A (MapRemove A m a)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H0. rewrite H0. reflexivity.
+    intro H0. elim (MapCard_Remove_2 m a (sym_eq H0)). intros y H1. rewrite H1 in H.
+    discriminate H.
+  Qed.
+
+  Lemma MapCard_Remove_2_conv :
+   forall (m:Map A) (a:ad) (y:A),
+     MapGet A m a = SOME A y -> S (MapCard A (MapRemove A m a)) = MapCard A m.
+  Proof.
+    intros.
+    elim
+     (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m)
+        (MapCard A (MapRemove A m a)) (refl_equal _) (
+        refl_equal _) (refl_equal _)).
+    intro H0. rewrite (MapCard_Remove_1 m a (sym_eq H0)) in H. discriminate H.
+    intro H0. rewrite H0. reflexivity.
+  Qed.
+
+  Lemma MapMerge_Restr_Card :
+   forall m m':Map A,
+     MapCard A m + MapCard A m' =
+     MapCard A (MapMerge A m m') + MapCard A (MapDomRestrTo A A m m').
+  Proof.
+    simple induction m. simpl in |- *. intro. apply plus_n_O.
+    simpl in |- *. intros a y m'. elim (option_sum A (MapGet A m' a)). intro H. elim H. intros y0 H0.
+    rewrite H0. rewrite MapCard_Put_behind_Put. rewrite (MapCard_Put_1_conv m' a y0 y H0).
+    simpl in |- *. rewrite <- plus_Snm_nSm. apply plus_n_O.
+    intro H. rewrite H. rewrite MapCard_Put_behind_Put. rewrite (MapCard_Put_2_conv m' a y H).
+    apply plus_n_O.
+    intros.
+    change
+      (MapCard A m0 + MapCard A m1 + MapCard A m' =
+       MapCard A (MapMerge A (M2 A m0 m1) m') +
+       MapCard A (MapDomRestrTo A A (M2 A m0 m1) m')) 
+     in |- *.
+    elim m'. reflexivity.
+    intros a y. unfold MapMerge in |- *. unfold MapDomRestrTo in |- *.
+    elim (option_sum A (MapGet A (M2 A m0 m1) a)). intro H1. elim H1. intros y0 H2. rewrite H2.
+    rewrite (MapCard_Put_1_conv (M2 A m0 m1) a y0 y H2). reflexivity.
+    intro H1. rewrite H1. rewrite (MapCard_Put_2_conv (M2 A m0 m1) a y H1). simpl in |- *.
+    rewrite <- (plus_Snm_nSm (MapCard A m0 + MapCard A m1) 0). reflexivity.
+    intros. simpl in |- *.
+    rewrite
+     (plus_permute_2_in_4 (MapCard A m0) (MapCard A m1) (
+        MapCard A m2) (MapCard A m3)).
+    rewrite (H m2). rewrite (H0 m3).
+    rewrite
+     (MapCard_makeM2 (MapDomRestrTo A A m0 m2) (MapDomRestrTo A A m1 m3))
+     .
+    apply plus_permute_2_in_4.
+  Qed.
+
+  Lemma MapMerge_disjoint_Card :
+   forall m m':Map A,
+     MapDisjoint A A m m' ->
+     MapCard A (MapMerge A m m') = MapCard A m + MapCard A m'.
+  Proof.
+    intros. rewrite (MapMerge_Restr_Card m m').
+    rewrite (MapCard_ext _ _ (MapDisjoint_imp_2 _ _ _ _ H)). apply plus_n_O.
+  Qed.
+
+  Lemma MapSplit_Card :
+   forall (m:Map A) (m':Map B),
+     MapCard A m =
+     MapCard A (MapDomRestrTo A B m m') + MapCard A (MapDomRestrBy A B m m').
+  Proof.
+    intros. rewrite (MapCard_ext _ _ (MapDom_Split_1 A B m m')). apply MapMerge_disjoint_Card.
+    apply MapDisjoint_2_imp. unfold MapDisjoint_2 in |- *. apply MapDom_Split_3.
+  Qed.
+
+  Lemma MapMerge_Card_ub :
+   forall m m':Map A,
+     MapCard A (MapMerge A m m') <= MapCard A m + MapCard A m'.
+  Proof.
+    intros. rewrite MapMerge_Restr_Card. apply le_plus_l.
+  Qed.
+
+  Lemma MapDomRestrTo_Card_ub_l :
+   forall (m:Map A) (m':Map B),
+     MapCard A (MapDomRestrTo A B m m') <= MapCard A m.
+  Proof.
+    intros. rewrite (MapSplit_Card m m'). apply le_plus_l.
+  Qed.
+
+  Lemma MapDomRestrBy_Card_ub_l :
+   forall (m:Map A) (m':Map B),
+     MapCard A (MapDomRestrBy A B m m') <= MapCard A m.
+  Proof.
+    intros. rewrite (MapSplit_Card m m'). apply le_plus_r.
+  Qed.
+
+  Lemma MapMerge_Card_disjoint :
+   forall m m':Map A,
+     MapCard A (MapMerge A m m') = MapCard A m + MapCard A m' ->
+     MapDisjoint A A m m'.
+  Proof.
+    simple induction m. intros. apply Map_M0_disjoint.
+    simpl in |- *. intros. rewrite (MapCard_Put_behind_Put m' a a0) in H. unfold MapDisjoint, in_dom in |- *.
+    simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H2.
+    rewrite (ad_eq_complete _ _ H2) in H. rewrite (MapCard_Put_2 m' a1 a0 H) in H1.
+    discriminate H1.
+    intro H2. rewrite H2 in H0. discriminate H0.
+    simple induction m'. intros. apply Map_disjoint_M0.
+    intros a y H1. rewrite <- (MapCard_ext _ _ (MapPut_as_Merge A (M2 A m0 m1) a y)) in H1.
+    unfold MapCard at 3 in H1. rewrite <- (plus_Snm_nSm (MapCard A (M2 A m0 m1)) 0) in H1.
+    rewrite <- (plus_n_O (S (MapCard A (M2 A m0 m1)))) in H1. unfold MapDisjoint, in_dom in |- *.
+    unfold MapGet at 2 in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)). intro H4.
+    rewrite <- (ad_eq_complete _ _ H4) in H2. rewrite (MapCard_Put_2 _ _ _ H1) in H2.
+    discriminate H2.
+    intro H4. rewrite H4 in H3. discriminate H3.
+    intros. unfold MapDisjoint in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H6.
+    unfold MapDisjoint in H0. apply H0 with (m' := m3) (a := ad_div_2 a). apply le_antisym.
+    apply MapMerge_Card_ub.
+    apply (fun p n m:nat => plus_le_reg_l n m p) with
+     (p := MapCard A m0 + MapCard A m2).
+    rewrite
+     (plus_permute_2_in_4 (MapCard A m0) (MapCard A m2) (
+        MapCard A m1) (MapCard A m3)).
+    change
+      (MapCard A (M2 A (MapMerge A m0 m2) (MapMerge A m1 m3)) =
+       MapCard A m0 + MapCard A m1 + (MapCard A m2 + MapCard A m3)) 
+     in H3.
+    rewrite <- H3. simpl in |- *. apply plus_le_compat_r. apply MapMerge_Card_ub.
+    elim (in_dom_some _ _ _ H4). intros y H7. rewrite (MapGet_M2_bit_0_1 _ a H6 m0 m1) in H7.
+    unfold in_dom in |- *. rewrite H7. reflexivity.
+    elim (in_dom_some _ _ _ H5). intros y H7. rewrite (MapGet_M2_bit_0_1 _ a H6 m2 m3) in H7.
+    unfold in_dom in |- *. rewrite H7. reflexivity.
+    intro H6. unfold MapDisjoint in H. apply H with (m' := m2) (a := ad_div_2 a). apply le_antisym.
+    apply MapMerge_Card_ub.
+    apply (fun p n m:nat => plus_le_reg_l n m p) with
+     (p := MapCard A m1 + MapCard A m3).
+    rewrite
+     (plus_comm (MapCard A m1 + MapCard A m3) (MapCard A m0 + MapCard A m2))
+     .
+    rewrite
+     (plus_permute_2_in_4 (MapCard A m0) (MapCard A m2) (
+        MapCard A m1) (MapCard A m3)).
+    rewrite
+     (plus_comm (MapCard A m1 + MapCard A m3) (MapCard A (MapMerge A m0 m2)))
+     .
+    change
+      (MapCard A (MapMerge A m0 m2) + MapCard A (MapMerge A m1 m3) =
+       MapCard A m0 + MapCard A m1 + (MapCard A m2 + MapCard A m3)) 
+     in H3.
+    rewrite <- H3. apply plus_le_compat_l. apply MapMerge_Card_ub.
+    elim (in_dom_some _ _ _ H4). intros y H7. rewrite (MapGet_M2_bit_0_0 _ a H6 m0 m1) in H7.
+    unfold in_dom in |- *. rewrite H7. reflexivity.
+    elim (in_dom_some _ _ _ H5). intros y H7. rewrite (MapGet_M2_bit_0_0 _ a H6 m2 m3) in H7.
+    unfold in_dom in |- *. rewrite H7. reflexivity.
+  Qed.
+
+  Lemma MapCard_is_Sn :
+   forall (m:Map A) (n:nat),
+     MapCard _ m = S n -> {a : ad | in_dom _ a m = true}.
+  Proof.
+    simple induction m. intros. discriminate H.
+    intros a y n H. split with a. unfold in_dom in |- *. rewrite (M1_semantics_1 _ a y). reflexivity.
+    intros. simpl in H1. elim (O_or_S (MapCard _ m0)). intro H2. elim H2. intros m2 H3.
+    elim (H _ (sym_eq H3)). intros a H4. split with (ad_double a). unfold in_dom in |- *.
+    rewrite (MapGet_M2_bit_0_0 A (ad_double a) (ad_double_bit_0 a) m0 m1).
+    rewrite (ad_double_div_2 a). elim (in_dom_some _ _ _ H4). intros y H5. rewrite H5. reflexivity.
+    intro H2. rewrite <- H2 in H1. simpl in H1. elim (H0 _ H1). intros a H3.
+    split with (ad_double_plus_un a). unfold in_dom in |- *.
+    rewrite
+     (MapGet_M2_bit_0_1 A (ad_double_plus_un a) (ad_double_plus_un_bit_0 a)
+        m0 m1).
+    rewrite (ad_double_plus_un_div_2 a). elim (in_dom_some _ _ _ H3). intros y H4. rewrite H4.
+    reflexivity.
   Qed.
 
 End MapCard.
 
 Section MapCard2.
 
-  Variable A, B : Set.
-
-  Lemma MapSubset_card_eq_1 : (n:nat) (m:(Map A)) (m':(Map B))
-      (MapSubset ? ? m m') -> (MapCard ? m)=n -> (MapCard ? m')=n ->
-        (MapSubset ? ? m' m).
-  Proof.
-    Induction n. Intros. Unfold MapSubset in_dom. Intro. Rewrite (MapCard_is_O ? m H0 a).
-    Rewrite (MapCard_is_O ? m' H1 a). Intro H2. Discriminate H2.
-    Intros. Elim (MapCard_is_Sn A m n0 H1). Intros a H3. Elim (in_dom_some ? ? ? H3).
-    Intros y H4. Elim (in_dom_some ? ? ? (H0 ? H3)). Intros y' H6.
-    Cut (eqmap ? (MapPut ? (MapRemove ? m a) a y) m). Intro.
-    Cut (eqmap ? (MapPut ? (MapRemove ? m' a) a y') m'). Intro.
-    Apply MapSubset_ext with m0:=(MapPut ? (MapRemove ? m' a) a y')
-                             m2:=(MapPut ? (MapRemove ? m a) a y).
-    Assumption.
-    Assumption.
-    Apply MapSubset_Put_mono. Apply H. Apply MapSubset_Remove_mono. Assumption.
-    Rewrite <- (MapCard_Remove_2_conv ? m a y H4) in H1. Inversion_clear H1. Reflexivity.
-    Rewrite <- (MapCard_Remove_2_conv ? m' a y' H6) in H2. Inversion_clear H2. Reflexivity.
-    Unfold eqmap eqm. Intro. Rewrite (MapPut_semantics ? (MapRemove B m' a) a y' a0).
-    Elim (sumbool_of_bool (ad_eq a a0)). Intro H7. Rewrite H7. Rewrite <- (ad_eq_complete ? ? H7).
-    Apply sym_eq. Assumption.
-    Intro H7. Rewrite H7. Rewrite (MapRemove_semantics ? m' a a0). Rewrite H7. Reflexivity.
-    Unfold eqmap eqm. Intro. Rewrite (MapPut_semantics ? (MapRemove A m a) a y a0).
-    Elim (sumbool_of_bool (ad_eq a a0)). Intro H7. Rewrite H7. Rewrite <- (ad_eq_complete ? ? H7).
-    Apply sym_eq. Assumption.
-    Intro H7. Rewrite H7. Rewrite (MapRemove_semantics A m a a0). Rewrite H7. Reflexivity.
-  Qed.
-
-  Lemma MapDomRestrTo_Card_ub_r : (m:(Map A)) (m':(Map B))
-      (le (MapCard A (MapDomRestrTo A B m m')) (MapCard B m')).
-  Proof.
-    Induction m. Intro. Simpl. Apply le_O_n.
-    Intros a y m'. Simpl. Elim (option_sum B (MapGet B m' a)). Intro H. Elim H. Intros y0 H0.
-    Rewrite H0. Elim (MapCard_is_not_O B m' a y0 H0). Intros n H1. Rewrite H1. Simpl.
-    Apply le_n_S. Apply le_O_n.
-    Intro H. Rewrite H. Simpl. Apply le_O_n.
-    Induction m'. Simpl. Apply le_O_n.
-
-    Intros a y. Unfold MapDomRestrTo. Case (MapGet A (M2 A m0 m1) a). Simpl. Apply le_O_n.
-    Intro. Simpl. Apply le_n.
-    Intros. Simpl. Rewrite (MapCard_makeM2 A (MapDomRestrTo A B m0 m2) (MapDomRestrTo A B m1 m3)).
-    Apply le_plus_plus. Apply H.
-    Apply H0.
+  Variables A B : Set.
+
+  Lemma MapSubset_card_eq_1 :
+   forall (n:nat) (m:Map A) (m':Map B),
+     MapSubset _ _ m m' ->
+     MapCard _ m = n -> MapCard _ m' = n -> MapSubset _ _ m' m.
+  Proof.
+    simple induction n. intros. unfold MapSubset, in_dom in |- *. intro. rewrite (MapCard_is_O _ m H0 a).
+    rewrite (MapCard_is_O _ m' H1 a). intro H2. discriminate H2.
+    intros. elim (MapCard_is_Sn A m n0 H1). intros a H3. elim (in_dom_some _ _ _ H3).
+    intros y H4. elim (in_dom_some _ _ _ (H0 _ H3)). intros y' H6.
+    cut (eqmap _ (MapPut _ (MapRemove _ m a) a y) m). intro.
+    cut (eqmap _ (MapPut _ (MapRemove _ m' a) a y') m'). intro.
+    apply MapSubset_ext with
+     (m0 := MapPut _ (MapRemove _ m' a) a y')
+     (m2 := MapPut _ (MapRemove _ m a) a y).
+    assumption.
+    assumption.
+    apply MapSubset_Put_mono. apply H. apply MapSubset_Remove_mono. assumption.
+    rewrite <- (MapCard_Remove_2_conv _ m a y H4) in H1. inversion_clear H1. reflexivity.
+    rewrite <- (MapCard_Remove_2_conv _ m' a y' H6) in H2. inversion_clear H2. reflexivity.
+    unfold eqmap, eqm in |- *. intro. rewrite (MapPut_semantics _ (MapRemove B m' a) a y' a0).
+    elim (sumbool_of_bool (ad_eq a a0)). intro H7. rewrite H7. rewrite <- (ad_eq_complete _ _ H7).
+    apply sym_eq. assumption.
+    intro H7. rewrite H7. rewrite (MapRemove_semantics _ m' a a0). rewrite H7. reflexivity.
+    unfold eqmap, eqm in |- *. intro. rewrite (MapPut_semantics _ (MapRemove A m a) a y a0).
+    elim (sumbool_of_bool (ad_eq a a0)). intro H7. rewrite H7. rewrite <- (ad_eq_complete _ _ H7).
+    apply sym_eq. assumption.
+    intro H7. rewrite H7. rewrite (MapRemove_semantics A m a a0). rewrite H7. reflexivity.
+  Qed.
+
+  Lemma MapDomRestrTo_Card_ub_r :
+   forall (m:Map A) (m':Map B),
+     MapCard A (MapDomRestrTo A B m m') <= MapCard B m'.
+  Proof.
+    simple induction m. intro. simpl in |- *. apply le_O_n.
+    intros a y m'. simpl in |- *. elim (option_sum B (MapGet B m' a)). intro H. elim H. intros y0 H0.
+    rewrite H0. elim (MapCard_is_not_O B m' a y0 H0). intros n H1. rewrite H1. simpl in |- *.
+    apply le_n_S. apply le_O_n.
+    intro H. rewrite H. simpl in |- *. apply le_O_n.
+    simple induction m'. simpl in |- *. apply le_O_n.
+
+    intros a y. unfold MapDomRestrTo in |- *. case (MapGet A (M2 A m0 m1) a). simpl in |- *. apply le_O_n.
+    intro. simpl in |- *. apply le_n.
+    intros. simpl in |- *. rewrite
+  (MapCard_makeM2 A (MapDomRestrTo A B m0 m2) (MapDomRestrTo A B m1 m3))
+  .
+    apply plus_le_compat. apply H.
+    apply H0.
   Qed.
 
 End MapCard2.
 
 Section MapCard3.
 
-  Variable A, B : Set.
+  Variables A B : Set.
 
-  Lemma MapMerge_Card_lb_l : (m,m':(Map A))
-      (ge (MapCard A (MapMerge A m m')) (MapCard A m)).
+  Lemma MapMerge_Card_lb_l :
+   forall m m':Map A, MapCard A (MapMerge A m m') >= MapCard A m.
   Proof.
-    Unfold ge. Intros. Apply (simpl_le_plus_l (MapCard A m')).
-    Rewrite (plus_sym (MapCard A m') (MapCard A m)).
-    Rewrite (plus_sym (MapCard A m') (MapCard A (MapMerge A m m'))).
-    Rewrite (MapMerge_Restr_Card A m m'). Apply le_reg_l. Apply MapDomRestrTo_Card_ub_r.
+    unfold ge in |- *. intros. apply ((fun p n m:nat => plus_le_reg_l n m p) (MapCard A m')).
+    rewrite (plus_comm (MapCard A m') (MapCard A m)).
+    rewrite (plus_comm (MapCard A m') (MapCard A (MapMerge A m m'))).
+    rewrite (MapMerge_Restr_Card A m m'). apply plus_le_compat_l. apply MapDomRestrTo_Card_ub_r.
   Qed.
 
-  Lemma MapMerge_Card_lb_r : (m,m':(Map A))
-      (ge (MapCard A (MapMerge A m m')) (MapCard A m')).
+  Lemma MapMerge_Card_lb_r :
+   forall m m':Map A, MapCard A (MapMerge A m m') >= MapCard A m'.
   Proof.
-    Unfold ge. Intros. Apply (simpl_le_plus_l (MapCard A m)). Rewrite (MapMerge_Restr_Card A m m').
-    Rewrite (plus_sym (MapCard A (MapMerge A m m')) (MapCard A (MapDomRestrTo A A m m'))).
-    Apply le_reg_r. Apply MapDomRestrTo_Card_ub_l.
+    unfold ge in |- *. intros. apply ((fun p n m:nat => plus_le_reg_l n m p) (MapCard A m)). rewrite (MapMerge_Restr_Card A m m').
+    rewrite
+     (plus_comm (MapCard A (MapMerge A m m'))
+        (MapCard A (MapDomRestrTo A A m m'))).
+    apply plus_le_compat_r. apply MapDomRestrTo_Card_ub_l.
   Qed.
 
-  Lemma MapDomRestrBy_Card_lb : (m:(Map A)) (m':(Map B))
-      (ge (plus (MapCard B m') (MapCard A (MapDomRestrBy A B m m'))) (MapCard A m)).
+  Lemma MapDomRestrBy_Card_lb :
+   forall (m:Map A) (m':Map B),
+     MapCard B m' + MapCard A (MapDomRestrBy A B m m') >= MapCard A m.
   Proof.
-    Unfold ge. Intros. Rewrite (MapSplit_Card A B m m'). Apply le_reg_r.
-    Apply MapDomRestrTo_Card_ub_r.
+    unfold ge in |- *. intros. rewrite (MapSplit_Card A B m m'). apply plus_le_compat_r.
+    apply MapDomRestrTo_Card_ub_r.
   Qed.
 
-  Lemma MapSubset_Card_le : (m:(Map A)) (m':(Map B))
-      (MapSubset A B m m') -> (le (MapCard A m) (MapCard B m')).
+  Lemma MapSubset_Card_le :
+   forall (m:Map A) (m':Map B),
+     MapSubset A B m m' -> MapCard A m <= MapCard B m'.
   Proof.
-    Intros. Apply le_trans with m:=(plus (MapCard B m') (MapCard A (MapDomRestrBy A B m m'))).
-    Exact (MapDomRestrBy_Card_lb m m').
-    Rewrite (MapCard_ext ? ? ? (MapSubset_imp_2 ? ? ? ? H)). Simpl. Rewrite <- plus_n_O.
-    Apply le_n.
+    intros. apply le_trans with (m := MapCard B m' + MapCard A (MapDomRestrBy A B m m')).
+    exact (MapDomRestrBy_Card_lb m m').
+    rewrite (MapCard_ext _ _ _ (MapSubset_imp_2 _ _ _ _ H)). simpl in |- *. rewrite <- plus_n_O.
+    apply le_n.
   Qed.
 
-  Lemma MapSubset_card_eq : (m:(Map A)) (m':(Map B))
-      (MapSubset ? ? m m') -> (le (MapCard ? m') (MapCard ? m)) ->
-        (eqmap ? (MapDom ? m) (MapDom ? m')).
+  Lemma MapSubset_card_eq :
+   forall (m:Map A) (m':Map B),
+     MapSubset _ _ m m' ->
+     MapCard _ m' <= MapCard _ m -> eqmap _ (MapDom _ m) (MapDom _ m').
   Proof.
-    Intros. Apply MapSubset_antisym. Assumption.
-    Cut (MapCard B m')=(MapCard A m). Intro. Apply (MapSubset_card_eq_1 A B (MapCard A m)).
-    Assumption.
-    Reflexivity.
-    Assumption.
-    Apply le_antisym. Assumption.
-    Apply MapSubset_Card_le. Assumption.
+    intros. apply MapSubset_antisym. assumption.
+    cut (MapCard B m' = MapCard A m). intro. apply (MapSubset_card_eq_1 A B (MapCard A m)).
+    assumption.
+    reflexivity.
+    assumption.
+    apply le_antisym. assumption.
+    apply MapSubset_Card_le. assumption.
   Qed.
 
-End MapCard3.
+End MapCard3.
\ No newline at end of file