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, 396 insertions, 344 deletions

diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v
index defe49712c..cff8f670bb 100644
--- a/theories/IntMap/Mapsubset.v
+++ b/theories/IntMap/Mapsubset.v
@@ -7,548 +7,600 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-Require Bool.
-Require Sumbool.
-Require Arith.
-Require ZArith.
-Require Addr.
-Require Adist.
-Require Addec.
-Require Map.
-Require Fset.
-Require Mapaxioms.
-Require Mapiter.
+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 Fset.
+Require Import Mapaxioms.
+Require Import Mapiter.
 
 Section MapSubsetDef.
 
-  Variable A, B : Set.
+  Variables A B : Set.
 
-  Definition MapSubset := [m:(Map A)] [m':(Map B)]
-      (a:ad) (in_dom A a m)=true -> (in_dom B a m')=true.
+  Definition MapSubset (m:Map A) (m':Map B) :=
+    forall a:ad, in_dom A a m = true -> in_dom B a m' = true.
 
-  Definition MapSubset_1 := [m:(Map A)] [m':(Map B)]
-      Cases (MapSweep A [a:ad][_:A] (negb (in_dom B a m')) m) of
-          NONE => true
-	| _ => false
-      end.
+  Definition MapSubset_1 (m:Map A) (m':Map B) :=
+    match MapSweep A (fun (a:ad) (_:A) => negb (in_dom B a m')) m with
+    | NONE => true
+    | _ => false
+    end.
 
-  Definition MapSubset_2 := [m:(Map A)] [m':(Map B)] 
-      (eqmap A (MapDomRestrBy A B m m') (M0 A)).
+  Definition MapSubset_2 (m:Map A) (m':Map B) :=
+    eqmap A (MapDomRestrBy A B m m') (M0 A).
 
-  Lemma MapSubset_imp_1 : (m:(Map A)) (m':(Map B))
-      (MapSubset m m') -> (MapSubset_1 m m')=true.
+  Lemma MapSubset_imp_1 :
+   forall (m:Map A) (m':Map B), MapSubset m m' -> MapSubset_1 m m' = true.
   Proof.
-    Unfold MapSubset MapSubset_1. Intros.
-    Elim (option_sum ? (MapSweep A [a:ad][_:A](negb (in_dom B a m')) m)).
-    Intro H0. Elim H0. Intro r. Elim r. Intros a y H1. Cut (negb (in_dom B a m'))=true.
-    Intro. Cut (in_dom A a m)=false. Intro. Unfold in_dom in H3.
-    Rewrite (MapSweep_semantics_2 ? ? m a y H1) in H3. Discriminate H3.
-    Elim (sumbool_of_bool (in_dom A a m)). Intro H3. Rewrite (H a H3) in H2. Discriminate H2.
-    Trivial.
-    Exact (MapSweep_semantics_1 ? ? m a y H1).
-    Intro H0. Rewrite H0. Reflexivity.
+    unfold MapSubset, MapSubset_1 in |- *. intros.
+    elim
+     (option_sum _ (MapSweep A (fun (a:ad) (_:A) => negb (in_dom B a m')) m)).
+    intro H0. elim H0. intro r. elim r. intros a y H1. cut (negb (in_dom B a m') = true).
+    intro. cut (in_dom A a m = false). intro. unfold in_dom in H3.
+    rewrite (MapSweep_semantics_2 _ _ m a y H1) in H3. discriminate H3.
+    elim (sumbool_of_bool (in_dom A a m)). intro H3. rewrite (H a H3) in H2. discriminate H2.
+    trivial.
+    exact (MapSweep_semantics_1 _ _ m a y H1).
+    intro H0. rewrite H0. reflexivity.
   Qed.
 
-  Lemma MapSubset_1_imp : (m:(Map A)) (m':(Map B))
-      (MapSubset_1 m m')=true -> (MapSubset m m').
+  Lemma MapSubset_1_imp :
+   forall (m:Map A) (m':Map B), MapSubset_1 m m' = true -> MapSubset m m'.
   Proof.
-    Unfold MapSubset MapSubset_1. Unfold 2 in_dom. Intros. Elim (option_sum ? (MapGet A m a)).
-    Intro H1. Elim H1. Intros y H2.
-    Elim (option_sum ? (MapSweep A [a:ad][_:A](negb (in_dom B a m')) m)). Intro H3.
-    Elim H3. Intro r. Elim r. Intros a' y' H4. Rewrite H4 in H. Discriminate H.
-    Intro H3. Cut (negb (in_dom B a m'))=false. Intro. Rewrite (negb_intro (in_dom B a m')).
-    Rewrite H4. Reflexivity.
-    Exact (MapSweep_semantics_3 ? ? m H3 a y H2).
-    Intro H1. Rewrite H1 in H0. Discriminate H0.
+    unfold MapSubset, MapSubset_1 in |- *. unfold in_dom at 2 in |- *. intros. elim (option_sum _ (MapGet A m a)).
+    intro H1. elim H1. intros y H2.
+    elim
+     (option_sum _ (MapSweep A (fun (a:ad) (_:A) => negb (in_dom B a m')) m)). intro H3.
+    elim H3. intro r. elim r. intros a' y' H4. rewrite H4 in H. discriminate H.
+    intro H3. cut (negb (in_dom B a m') = false). intro. rewrite (negb_intro (in_dom B a m')).
+    rewrite H4. reflexivity.
+    exact (MapSweep_semantics_3 _ _ m H3 a y H2).
+    intro H1. rewrite H1 in H0. discriminate H0.
   Qed.
 
-  Lemma map_dom_empty_1 : 
-      (m:(Map A)) (eqmap A m (M0 A)) -> (a:ad) (in_dom ? a m)=false.
+  Lemma map_dom_empty_1 :
+   forall m:Map A, eqmap A m (M0 A) -> forall a:ad, in_dom _ a m = false.
   Proof.
-    Unfold eqmap eqm in_dom. Intros. Rewrite (H a). Reflexivity.
+    unfold eqmap, eqm, in_dom in |- *. intros. rewrite (H a). reflexivity.
   Qed.
 
-  Lemma map_dom_empty_2 : 
-      (m:(Map A)) ((a:ad) (in_dom ? a m)=false) -> (eqmap A m (M0 A)).
+  Lemma map_dom_empty_2 :
+   forall m:Map A, (forall a:ad, in_dom _ a m = false) -> eqmap A m (M0 A).
   Proof.
-    Unfold eqmap eqm in_dom. Intros.
-    Cut (Cases (MapGet A m a) of NONE => false | (SOME _) => true end)=false.
-    Case (MapGet A m a). Trivial.
-    Intros. Discriminate H0.
-    Exact (H a).
+    unfold eqmap, eqm, in_dom in |- *. intros.
+    cut
+     (match MapGet A m a with
+      | NONE => false
+      | SOME _ => true
+      end = false).
+    case (MapGet A m a). trivial.
+    intros. discriminate H0.
+    exact (H a).
   Qed.
 
-  Lemma MapSubset_imp_2 : 
-      (m:(Map A)) (m':(Map B)) (MapSubset m m') -> (MapSubset_2 m m').
+  Lemma MapSubset_imp_2 :
+   forall (m:Map A) (m':Map B), MapSubset m m' -> MapSubset_2 m m'.
   Proof.
-    Unfold MapSubset MapSubset_2. Intros. Apply map_dom_empty_2. Intro. Rewrite in_dom_restrby.
-    Elim (sumbool_of_bool (in_dom A a m)). Intro H0. Rewrite H0. Rewrite (H a H0). Reflexivity.
-    Intro H0. Rewrite H0. Reflexivity.
+    unfold MapSubset, MapSubset_2 in |- *. intros. apply map_dom_empty_2. intro. rewrite in_dom_restrby.
+    elim (sumbool_of_bool (in_dom A a m)). intro H0. rewrite H0. rewrite (H a H0). reflexivity.
+    intro H0. rewrite H0. reflexivity.
   Qed.
 
-  Lemma MapSubset_2_imp : 
-      (m:(Map A)) (m':(Map B)) (MapSubset_2 m m') -> (MapSubset m m').
+  Lemma MapSubset_2_imp :
+   forall (m:Map A) (m':Map B), MapSubset_2 m m' -> MapSubset m m'.
   Proof.
-    Unfold MapSubset MapSubset_2. Intros. Cut (in_dom ? a (MapDomRestrBy A B m m'))=false.
-    Rewrite in_dom_restrby. Intro. Elim (andb_false_elim ? ? H1). Rewrite H0.
-    Intro H2. Discriminate H2.
-    Intro H2. Rewrite (negb_intro (in_dom B a m')). Rewrite H2. Reflexivity.
-    Exact (map_dom_empty_1 ? H a).
+    unfold MapSubset, MapSubset_2 in |- *. intros. cut (in_dom _ a (MapDomRestrBy A B m m') = false).
+    rewrite in_dom_restrby. intro. elim (andb_false_elim _ _ H1). rewrite H0.
+    intro H2. discriminate H2.
+    intro H2. rewrite (negb_intro (in_dom B a m')). rewrite H2. reflexivity.
+    exact (map_dom_empty_1 _ H a).
   Qed.
 
 End MapSubsetDef.
 
 Section MapSubsetOrder.
 
-  Variable A, B, C : Set.
+  Variables A B C : Set.
 
-  Lemma MapSubset_refl : (m:(Map A)) (MapSubset A A m m).
+  Lemma MapSubset_refl : forall m:Map A, MapSubset A A m m.
   Proof.
-      Unfold MapSubset. Trivial.
+      unfold MapSubset in |- *. trivial.
   Qed.
 
-  Lemma MapSubset_antisym : (m:(Map A)) (m':(Map B))
-      (MapSubset A B m m') -> (MapSubset B A m' m) -> 
-        (eqmap unit (MapDom A m) (MapDom B m')).
+  Lemma MapSubset_antisym :
+   forall (m:Map A) (m':Map B),
+     MapSubset A B m m' ->
+     MapSubset B A m' m -> eqmap unit (MapDom A m) (MapDom B m').
   Proof.
-    Unfold MapSubset eqmap eqm. Intros. Elim (option_sum ? (MapGet ? (MapDom A m) a)).
-    Intro H1. Elim H1. Intro t. Elim t. Intro H2. Elim (option_sum ? (MapGet ? (MapDom B m') a)).
-    Intro H3. Elim H3. Intro t'. Elim t'. Intro H4. Rewrite H4. Exact H2. 
-    Intro H3. Cut (in_dom B a m')=true. Intro. Rewrite (MapDom_Dom B m' a) in H4.
-    Unfold in_FSet in_dom in H4. Rewrite H3 in H4. Discriminate H4.
-    Apply H. Rewrite (MapDom_Dom A m a). Unfold in_FSet in_dom. Rewrite H2. Reflexivity.
-    Intro H1. Elim (option_sum ? (MapGet ? (MapDom B m') a)). Intro H2. Elim H2. Intros t H3.
-    Cut (in_dom A a m)=true. Intro. Rewrite (MapDom_Dom A m a) in H4. Unfold in_FSet in_dom in H4.
-    Rewrite H1 in H4. Discriminate H4.
-    Apply H0. Rewrite (MapDom_Dom B m' a). Unfold in_FSet in_dom. Rewrite H3. Reflexivity.
-    Intro H2. Rewrite H2. Exact H1.
+    unfold MapSubset, eqmap, eqm in |- *. intros. elim (option_sum _ (MapGet _ (MapDom A m) a)).
+    intro H1. elim H1. intro t. elim t. intro H2. elim (option_sum _ (MapGet _ (MapDom B m') a)).
+    intro H3. elim H3. intro t'. elim t'. intro H4. rewrite H4. exact H2. 
+    intro H3. cut (in_dom B a m' = true). intro. rewrite (MapDom_Dom B m' a) in H4.
+    unfold in_FSet, in_dom in H4. rewrite H3 in H4. discriminate H4.
+    apply H. rewrite (MapDom_Dom A m a). unfold in_FSet, in_dom in |- *. rewrite H2. reflexivity.
+    intro H1. elim (option_sum _ (MapGet _ (MapDom B m') a)). intro H2. elim H2. intros t H3.
+    cut (in_dom A a m = true). intro. rewrite (MapDom_Dom A m a) in H4. unfold in_FSet, in_dom in H4.
+    rewrite H1 in H4. discriminate H4.
+    apply H0. rewrite (MapDom_Dom B m' a). unfold in_FSet, in_dom in |- *. rewrite H3. reflexivity.
+    intro H2. rewrite H2. exact H1.
   Qed.
 
-  Lemma MapSubset_trans : (m:(Map A)) (m':(Map B)) (m'':(Map C))
-      (MapSubset A B m m') -> (MapSubset B C m' m'') -> (MapSubset A C m m'').
+  Lemma MapSubset_trans :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     MapSubset A B m m' -> MapSubset B C m' m'' -> MapSubset A C m m''.
   Proof.
-    Unfold MapSubset. Intros. Apply H0. Apply H. Assumption.
+    unfold MapSubset in |- *. intros. apply H0. apply H. assumption.
   Qed.
 
 End MapSubsetOrder.
 
 Section FSubsetOrder.
 
-  Lemma FSubset_refl : (s:FSet) (MapSubset ? ? s s).
+  Lemma FSubset_refl : forall s:FSet, MapSubset _ _ s s.
   Proof.
-    Exact (MapSubset_refl unit).
+    exact (MapSubset_refl unit).
   Qed.
 
-  Lemma FSubset_antisym : (s,s':FSet)
-      (MapSubset ? ? s s') -> (MapSubset ? ? s' s) -> (eqmap unit s s').
+  Lemma FSubset_antisym :
+   forall s s':FSet,
+     MapSubset _ _ s s' -> MapSubset _ _ s' s -> eqmap unit s s'.
   Proof.
-    Intros. Rewrite <- (FSet_Dom s). Rewrite <- (FSet_Dom s').
-    Exact (MapSubset_antisym ? ? s s' H H0).
+    intros. rewrite <- (FSet_Dom s). rewrite <- (FSet_Dom s').
+    exact (MapSubset_antisym _ _ s s' H H0).
   Qed.
 
-  Lemma FSubset_trans : (s,s',s'':FSet)
-      (MapSubset ? ? s s') -> (MapSubset ? ? s' s'') -> (MapSubset ? ? s s'').
+  Lemma FSubset_trans :
+   forall s s' s'':FSet,
+     MapSubset _ _ s s' -> MapSubset _ _ s' s'' -> MapSubset _ _ s s''.
   Proof.
-    Exact (MapSubset_trans unit unit unit).
+    exact (MapSubset_trans unit unit unit).
   Qed.
 
 End FSubsetOrder.
 
 Section MapSubsetExtra.
 
-  Variable A, B : Set.
+  Variables A B : Set.
 
-  Lemma MapSubset_Dom_1 : (m:(Map A)) (m':(Map B))
-      (MapSubset A B m m') -> (MapSubset unit unit (MapDom A m) (MapDom B m')).
+  Lemma MapSubset_Dom_1 :
+   forall (m:Map A) (m':Map B),
+     MapSubset A B m m' -> MapSubset unit unit (MapDom A m) (MapDom B m').
   Proof.
-    Unfold MapSubset. Intros. Elim (MapDom_semantics_2 ? m a H0). Intros y H1.
-    Cut (in_dom A a m)=true->(in_dom B a m')=true. Intro. Unfold in_dom in H2.
-    Rewrite H1 in H2. Elim (option_sum ? (MapGet B m' a)). Intro H3. Elim H3.
-    Intros y' H4. Exact (MapDom_semantics_1 ? m' a y' H4).
-    Intro H3. Rewrite H3 in H2. Cut false=true. Intro. Discriminate H4.
-    Apply H2. Reflexivity.
-    Exact (H a).
+    unfold MapSubset in |- *. intros. elim (MapDom_semantics_2 _ m a H0). intros y H1.
+    cut (in_dom A a m = true -> in_dom B a m' = true). intro. unfold in_dom in H2.
+    rewrite H1 in H2. elim (option_sum _ (MapGet B m' a)). intro H3. elim H3.
+    intros y' H4. exact (MapDom_semantics_1 _ m' a y' H4).
+    intro H3. rewrite H3 in H2. cut (false = true). intro. discriminate H4.
+    apply H2. reflexivity.
+    exact (H a).
   Qed.
 
-  Lemma MapSubset_Dom_2 : (m:(Map A)) (m':(Map B))
-      (MapSubset unit unit (MapDom A m) (MapDom B m')) -> (MapSubset A B m m').
+  Lemma MapSubset_Dom_2 :
+   forall (m:Map A) (m':Map B),
+     MapSubset unit unit (MapDom A m) (MapDom B m') -> MapSubset A B m m'.
   Proof.
-    Unfold MapSubset. Intros. Unfold in_dom in H0. Elim (option_sum ? (MapGet A m a)).
-    Intro H1. Elim H1. Intros y H2.
-    Elim (MapDom_semantics_2 ? ? ? (H a (MapDom_semantics_1 ? ? ? ? H2))). Intros y' H3.
-    Unfold in_dom. Rewrite H3. Reflexivity.
-    Intro H1. Rewrite H1 in H0. Discriminate H0.
+    unfold MapSubset in |- *. intros. unfold in_dom in H0. elim (option_sum _ (MapGet A m a)).
+    intro H1. elim H1. intros y H2.
+    elim (MapDom_semantics_2 _ _ _ (H a (MapDom_semantics_1 _ _ _ _ H2))). intros y' H3.
+    unfold in_dom in |- *. rewrite H3. reflexivity.
+    intro H1. rewrite H1 in H0. discriminate H0.
   Qed.
 
-  Lemma MapSubset_1_Dom : (m:(Map A)) (m':(Map B))
-      (MapSubset_1 A B m m')=(MapSubset_1 unit unit (MapDom A m) (MapDom B m')).
+  Lemma MapSubset_1_Dom :
+   forall (m:Map A) (m':Map B),
+     MapSubset_1 A B m m' = MapSubset_1 unit unit (MapDom A m) (MapDom B m').
   Proof.
-    Intros. Elim (sumbool_of_bool (MapSubset_1 A B m m')). Intro H. Rewrite H.
-    Apply sym_eq. Apply MapSubset_imp_1. Apply MapSubset_Dom_1. Exact (MapSubset_1_imp ? ? ? ? H).
-    Intro H. Rewrite H. Elim (sumbool_of_bool (MapSubset_1 unit unit (MapDom A m) (MapDom B m'))).
-    Intro H0.
-    Rewrite (MapSubset_imp_1 ? ? ? ? (MapSubset_Dom_2 ? ? (MapSubset_1_imp ? ? ? ? H0))) in H.
-    Discriminate H.
-    Intro. Apply sym_eq. Assumption.
+    intros. elim (sumbool_of_bool (MapSubset_1 A B m m')). intro H. rewrite H.
+    apply sym_eq. apply MapSubset_imp_1. apply MapSubset_Dom_1. exact (MapSubset_1_imp _ _ _ _ H).
+    intro H. rewrite H. elim (sumbool_of_bool (MapSubset_1 unit unit (MapDom A m) (MapDom B m'))).
+    intro H0.
+    rewrite
+     (MapSubset_imp_1 _ _ _ _
+        (MapSubset_Dom_2 _ _ (MapSubset_1_imp _ _ _ _ H0)))
+      in H.
+    discriminate H.
+    intro. apply sym_eq. assumption.
   Qed.
 
-  Lemma MapSubset_Put : (m:(Map A)) (a:ad) (y:A) (MapSubset A A m (MapPut A m a y)).
+  Lemma MapSubset_Put :
+   forall (m:Map A) (a:ad) (y:A), MapSubset A A m (MapPut A m a y).
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_put. Rewrite H. Apply orb_b_true.
+    unfold MapSubset in |- *. intros. rewrite in_dom_put. rewrite H. apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_Put_mono : (m:(Map A)) (m':(Map B)) (a:ad) (y:A) (y':B)
-      (MapSubset A B m m') -> (MapSubset A B (MapPut A m a y) (MapPut B m' a y')).
+  Lemma MapSubset_Put_mono :
+   forall (m:Map A) (m':Map B) (a:ad) (y:A) (y':B),
+     MapSubset A B m m' -> MapSubset A B (MapPut A m a y) (MapPut B m' a y').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_put. Rewrite (in_dom_put A m a y a0) in H0.
-    Elim (orb_true_elim ? ? H0). Intro H1. Rewrite H1. Reflexivity.
-    Intro H1. Rewrite (H ? H1). Apply orb_b_true.
+    unfold MapSubset in |- *. intros. rewrite in_dom_put. rewrite (in_dom_put A m a y a0) in H0.
+    elim (orb_true_elim _ _ H0). intro H1. rewrite H1. reflexivity.
+    intro H1. rewrite (H _ H1). apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_Put_behind : 
-      (m:(Map A)) (a:ad) (y:A) (MapSubset A A m (MapPut_behind A m a y)).
+  Lemma MapSubset_Put_behind :
+   forall (m:Map A) (a:ad) (y:A), MapSubset A A m (MapPut_behind A m a y).
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_put_behind. Rewrite H. Apply orb_b_true.
+    unfold MapSubset in |- *. intros. rewrite in_dom_put_behind. rewrite H. apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_Put_behind_mono : (m:(Map A)) (m':(Map B)) (a:ad) (y:A) (y':B)
-      (MapSubset A B m m') -> 
-        (MapSubset A B (MapPut_behind A m a y) (MapPut_behind B m' a y')).
+  Lemma MapSubset_Put_behind_mono :
+   forall (m:Map A) (m':Map B) (a:ad) (y:A) (y':B),
+     MapSubset A B m m' ->
+     MapSubset A B (MapPut_behind A m a y) (MapPut_behind B m' a y').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_put_behind.
-    Rewrite (in_dom_put_behind A m a y a0) in H0.
-    Elim (orb_true_elim ? ? H0). Intro H1. Rewrite H1. Reflexivity.
-    Intro H1. Rewrite (H ? H1). Apply orb_b_true.
+    unfold MapSubset in |- *. intros. rewrite in_dom_put_behind.
+    rewrite (in_dom_put_behind A m a y a0) in H0.
+    elim (orb_true_elim _ _ H0). intro H1. rewrite H1. reflexivity.
+    intro H1. rewrite (H _ H1). apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_Remove : (m:(Map A)) (a:ad) (MapSubset A A (MapRemove A m a) m).
+  Lemma MapSubset_Remove :
+   forall (m:Map A) (a:ad), MapSubset A A (MapRemove A m a) m.
   Proof.
-    Unfold MapSubset. Intros. Unfold MapSubset. Intros. Rewrite (in_dom_remove ? m a a0) in H.
-    Elim (andb_prop ? ? H). Trivial.
+    unfold MapSubset in |- *. intros. unfold MapSubset in |- *. intros. rewrite (in_dom_remove _ m a a0) in H.
+    elim (andb_prop _ _ H). trivial.
   Qed.
 
-  Lemma MapSubset_Remove_mono : (m:(Map A)) (m':(Map B)) (a:ad)
-      (MapSubset A B m m') -> (MapSubset A B (MapRemove A m a) (MapRemove B m' a)).
+  Lemma MapSubset_Remove_mono :
+   forall (m:Map A) (m':Map B) (a:ad),
+     MapSubset A B m m' -> MapSubset A B (MapRemove A m a) (MapRemove B m' a).
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_remove. Rewrite (in_dom_remove A m a a0) in H0.
-    Elim (andb_prop ? ? H0). Intros. Rewrite H1. Rewrite (H ? H2). Reflexivity.
+    unfold MapSubset in |- *. intros. rewrite in_dom_remove. rewrite (in_dom_remove A m a a0) in H0.
+    elim (andb_prop _ _ H0). intros. rewrite H1. rewrite (H _ H2). reflexivity.
   Qed.
 
-  Lemma MapSubset_Merge_l : (m,m':(Map A)) (MapSubset A A m (MapMerge A m m')).
+  Lemma MapSubset_Merge_l :
+   forall m m':Map A, MapSubset A A m (MapMerge A m m').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_merge. Rewrite H. Reflexivity.
+    unfold MapSubset in |- *. intros. rewrite in_dom_merge. rewrite H. reflexivity.
   Qed.
 
-  Lemma MapSubset_Merge_r : (m,m':(Map A)) (MapSubset A A m' (MapMerge A m m')).
+  Lemma MapSubset_Merge_r :
+   forall m m':Map A, MapSubset A A m' (MapMerge A m m').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_merge. Rewrite H. Apply orb_b_true.
+    unfold MapSubset in |- *. intros. rewrite in_dom_merge. rewrite H. apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_Merge_mono : (m,m':(Map A)) (m'',m''':(Map B))
-      (MapSubset A B m m'') -> (MapSubset A B m' m''') ->
-      	(MapSubset A B (MapMerge A m m') (MapMerge B m'' m''')).
+  Lemma MapSubset_Merge_mono :
+   forall (m m':Map A) (m'' m''':Map B),
+     MapSubset A B m m'' ->
+     MapSubset A B m' m''' ->
+     MapSubset A B (MapMerge A m m') (MapMerge B m'' m''').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_merge. Rewrite (in_dom_merge A m m' a) in H1.
-    Elim (orb_true_elim ? ? H1). Intro H2. Rewrite (H ? H2). Reflexivity.
-    Intro H2. Rewrite (H0 ? H2). Apply orb_b_true.
+    unfold MapSubset in |- *. intros. rewrite in_dom_merge. rewrite (in_dom_merge A m m' a) in H1.
+    elim (orb_true_elim _ _ H1). intro H2. rewrite (H _ H2). reflexivity.
+    intro H2. rewrite (H0 _ H2). apply orb_b_true.
   Qed.
 
-  Lemma MapSubset_DomRestrTo_l : (m:(Map A)) (m':(Map B))
-      (MapSubset A A (MapDomRestrTo A B m m') m).
+  Lemma MapSubset_DomRestrTo_l :
+   forall (m:Map A) (m':Map B), MapSubset A A (MapDomRestrTo A B m m') m.
   Proof.
-    Unfold MapSubset. Intros. Rewrite (in_dom_restrto ? ? m m' a) in H. Elim (andb_prop ? ? H).
-    Trivial.
+    unfold MapSubset in |- *. intros. rewrite (in_dom_restrto _ _ m m' a) in H. elim (andb_prop _ _ H).
+    trivial.
   Qed.
 
-  Lemma MapSubset_DomRestrTo_r: (m:(Map A)) (m':(Map B))
-      (MapSubset A B (MapDomRestrTo A B m m') m').
+  Lemma MapSubset_DomRestrTo_r :
+   forall (m:Map A) (m':Map B), MapSubset A B (MapDomRestrTo A B m m') m'.
   Proof.
-    Unfold MapSubset. Intros. Rewrite (in_dom_restrto ? ? m m' a) in H. Elim (andb_prop ? ? H).
-    Trivial.
+    unfold MapSubset in |- *. intros. rewrite (in_dom_restrto _ _ m m' a) in H. elim (andb_prop _ _ H).
+    trivial.
   Qed.
 
-  Lemma MapSubset_ext : (m0,m1:(Map A)) (m2,m3:(Map B))
-      (eqmap A m0 m1) -> (eqmap B m2 m3) ->
-        (MapSubset A B m0 m2) -> (MapSubset A B m1 m3).
+  Lemma MapSubset_ext :
+   forall (m0 m1:Map A) (m2 m3:Map B),
+     eqmap A m0 m1 ->
+     eqmap B m2 m3 -> MapSubset A B m0 m2 -> MapSubset A B m1 m3.
   Proof.
-    Intros. Apply MapSubset_2_imp. Unfold MapSubset_2.
-    Apply eqmap_trans with m':=(MapDomRestrBy A B m0 m2). Apply MapDomRestrBy_ext. Apply eqmap_sym.
-    Assumption.
-    Apply eqmap_sym. Assumption.
-    Exact (MapSubset_imp_2 ? ? ? ? H1).
+    intros. apply MapSubset_2_imp. unfold MapSubset_2 in |- *.
+    apply eqmap_trans with (m' := MapDomRestrBy A B m0 m2). apply MapDomRestrBy_ext. apply eqmap_sym.
+    assumption.
+    apply eqmap_sym. assumption.
+    exact (MapSubset_imp_2 _ _ _ _ H1).
   Qed.
 
-  Variable C, D : Set.
+  Variables C D : Set.
 
-  Lemma MapSubset_DomRestrTo_mono : 
-      (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
-        (MapSubset ? ? m m'') -> (MapSubset ? ?  m' m''') ->
-      	  (MapSubset ? ? (MapDomRestrTo ? ? m m') (MapDomRestrTo ? ? m'' m''')).
+  Lemma MapSubset_DomRestrTo_mono :
+   forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
+     MapSubset _ _ m m'' ->
+     MapSubset _ _ m' m''' ->
+     MapSubset _ _ (MapDomRestrTo _ _ m m') (MapDomRestrTo _ _ m'' m''').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_restrto. Rewrite (in_dom_restrto A B m m' a) in H1.
-    Elim (andb_prop ? ? H1). Intros. Rewrite (H ? H2). Rewrite (H0 ? H3). Reflexivity.
+    unfold MapSubset in |- *. intros. rewrite in_dom_restrto. rewrite (in_dom_restrto A B m m' a) in H1.
+    elim (andb_prop _ _ H1). intros. rewrite (H _ H2). rewrite (H0 _ H3). reflexivity.
   Qed.
 
-  Lemma MapSubset_DomRestrBy_l : (m:(Map A)) (m':(Map B))
-      (MapSubset A A (MapDomRestrBy A B m m') m).
+  Lemma MapSubset_DomRestrBy_l :
+   forall (m:Map A) (m':Map B), MapSubset A A (MapDomRestrBy A B m m') m.
   Proof.
-    Unfold MapSubset. Intros. Rewrite (in_dom_restrby ? ? m m' a) in H. Elim (andb_prop ? ? H).
-    Trivial.
+    unfold MapSubset in |- *. intros. rewrite (in_dom_restrby _ _ m m' a) in H. elim (andb_prop _ _ H).
+    trivial.
   Qed.
 
-  Lemma MapSubset_DomRestrBy_mono : 
-      (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
-        (MapSubset ? ? m m'') -> (MapSubset ? ?  m''' m') ->
-      	  (MapSubset ? ? (MapDomRestrBy ? ? m m') (MapDomRestrBy ? ? m'' m''')).
+  Lemma MapSubset_DomRestrBy_mono :
+   forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
+     MapSubset _ _ m m'' ->
+     MapSubset _ _ m''' m' ->
+     MapSubset _ _ (MapDomRestrBy _ _ m m') (MapDomRestrBy _ _ m'' m''').
   Proof.
-    Unfold MapSubset. Intros. Rewrite in_dom_restrby. Rewrite (in_dom_restrby A B m m' a) in H1.
-    Elim (andb_prop ? ? H1). Intros. Rewrite (H ? H2). Elim (sumbool_of_bool (in_dom D a m''')).
-    Intro H4. Rewrite (H0 ? H4) in H3. Discriminate H3.
-    Intro H4. Rewrite H4. Reflexivity.
+    unfold MapSubset in |- *. intros. rewrite in_dom_restrby. rewrite (in_dom_restrby A B m m' a) in H1.
+    elim (andb_prop _ _ H1). intros. rewrite (H _ H2). elim (sumbool_of_bool (in_dom D a m''')).
+    intro H4. rewrite (H0 _ H4) in H3. discriminate H3.
+    intro H4. rewrite H4. reflexivity.
   Qed.
   
 End MapSubsetExtra.
 
 Section MapDisjointDef.
 
-  Variable A, B : Set.
+  Variables A B : Set.
 
-  Definition MapDisjoint := [m:(Map A)] [m':(Map B)]
-      (a:ad) (in_dom A a m)=true -> (in_dom B a m')=true -> False.
+  Definition MapDisjoint (m:Map A) (m':Map B) :=
+    forall a:ad, in_dom A a m = true -> in_dom B a m' = true -> False.
 
-  Definition MapDisjoint_1 := [m:(Map A)] [m':(Map B)]
-      Cases (MapSweep A [a:ad][_:A] (in_dom B a m') m) of
-          NONE => true
-	| _ => false
-      end.
+  Definition MapDisjoint_1 (m:Map A) (m':Map B) :=
+    match MapSweep A (fun (a:ad) (_:A) => in_dom B a m') m with
+    | NONE => true
+    | _ => false
+    end.
 
-  Definition MapDisjoint_2 := [m:(Map A)] [m':(Map B)] 
-      (eqmap A (MapDomRestrTo A B m m') (M0 A)).
+  Definition MapDisjoint_2 (m:Map A) (m':Map B) :=
+    eqmap A (MapDomRestrTo A B m m') (M0 A).
 
-  Lemma MapDisjoint_imp_1 : (m:(Map A)) (m':(Map B))
-      (MapDisjoint m m') -> (MapDisjoint_1 m m')=true.
+  Lemma MapDisjoint_imp_1 :
+   forall (m:Map A) (m':Map B), MapDisjoint m m' -> MapDisjoint_1 m m' = true.
   Proof.
-    Unfold MapDisjoint MapDisjoint_1. Intros.
-    Elim (option_sum ? (MapSweep A [a:ad][_:A](in_dom B a m') m)). Intro H0. Elim H0.
-    Intro r. Elim r. Intros a y H1. Cut (in_dom A a m)=true->(in_dom B a m')=true->False.
-    Intro. Unfold 1 in_dom in H2. Rewrite (MapSweep_semantics_2 ? ? ? ? ? H1) in H2.
-    Rewrite (MapSweep_semantics_1 ? ? ? ? ? H1) in H2. Elim (H2 (refl_equal ? ?) (refl_equal ? ?)).
-    Exact (H a).
-    Intro H0. Rewrite H0. Reflexivity.
+    unfold MapDisjoint, MapDisjoint_1 in |- *. intros.
+    elim (option_sum _ (MapSweep A (fun (a:ad) (_:A) => in_dom B a m') m)). intro H0. elim H0.
+    intro r. elim r. intros a y H1. cut (in_dom A a m = true -> in_dom B a m' = true -> False).
+    intro. unfold in_dom at 1 in H2. rewrite (MapSweep_semantics_2 _ _ _ _ _ H1) in H2.
+    rewrite (MapSweep_semantics_1 _ _ _ _ _ H1) in H2. elim (H2 (refl_equal _) (refl_equal _)).
+    exact (H a).
+    intro H0. rewrite H0. reflexivity.
   Qed.
 
-  Lemma MapDisjoint_1_imp : (m:(Map A)) (m':(Map B))
-      (MapDisjoint_1 m m')=true -> (MapDisjoint m m').
+  Lemma MapDisjoint_1_imp :
+   forall (m:Map A) (m':Map B), MapDisjoint_1 m m' = true -> MapDisjoint m m'.
   Proof.
-    Unfold MapDisjoint MapDisjoint_1. Intros.
-    Elim (option_sum ? (MapSweep A [a:ad][_:A](in_dom B a m') m)). Intro H2. Elim H2.
-    Intro r. Elim r. Intros a' y' H3. Rewrite H3 in H. Discriminate H.
-    Intro H2. Unfold in_dom in H0. Elim (option_sum ? (MapGet A m a)). Intro H3. Elim H3.
-    Intros y H4. Rewrite (MapSweep_semantics_3 ? ? ? H2 a y H4) in H1. Discriminate H1.
-    Intro H3. Rewrite H3 in H0. Discriminate H0.
+    unfold MapDisjoint, MapDisjoint_1 in |- *. intros.
+    elim (option_sum _ (MapSweep A (fun (a:ad) (_:A) => in_dom B a m') m)). intro H2. elim H2.
+    intro r. elim r. intros a' y' H3. rewrite H3 in H. discriminate H.
+    intro H2. unfold in_dom in H0. elim (option_sum _ (MapGet A m a)). intro H3. elim H3.
+    intros y H4. rewrite (MapSweep_semantics_3 _ _ _ H2 a y H4) in H1. discriminate H1.
+    intro H3. rewrite H3 in H0. discriminate H0.
   Qed.
 
-  Lemma MapDisjoint_imp_2 : (m:(Map A)) (m':(Map B)) (MapDisjoint m m') -> 
-      (MapDisjoint_2 m m').
+  Lemma MapDisjoint_imp_2 :
+   forall (m:Map A) (m':Map B), MapDisjoint m m' -> MapDisjoint_2 m m'.
   Proof.
-    Unfold MapDisjoint MapDisjoint_2. Unfold eqmap eqm. Intros.
-    Rewrite (MapDomRestrTo_semantics A B m m' a).
-    Cut (in_dom A a m)=true->(in_dom B a m')=true->False. Intro.
-    Elim (option_sum ? (MapGet A m a)). Intro H1. Elim H1. Intros y H2. Unfold 1 in_dom in H0.
-    Elim (option_sum ? (MapGet B m' a)). Intro H3. Elim H3. Intros y' H4. Unfold 1 in_dom in H0.
-    Rewrite H4 in H0. Rewrite H2 in H0. Elim (H0 (refl_equal ? ?) (refl_equal ? ?)).
-    Intro H3. Rewrite H3. Reflexivity.
-    Intro H1. Rewrite H1. Case (MapGet B m' a); Reflexivity.
-    Exact (H a).
+    unfold MapDisjoint, MapDisjoint_2 in |- *. unfold eqmap, eqm in |- *. intros.
+    rewrite (MapDomRestrTo_semantics A B m m' a).
+    cut (in_dom A a m = true -> in_dom B a m' = true -> False). intro.
+    elim (option_sum _ (MapGet A m a)). intro H1. elim H1. intros y H2. unfold in_dom at 1 in H0.
+    elim (option_sum _ (MapGet B m' a)). intro H3. elim H3. intros y' H4. unfold in_dom at 1 in H0.
+    rewrite H4 in H0. rewrite H2 in H0. elim (H0 (refl_equal _) (refl_equal _)).
+    intro H3. rewrite H3. reflexivity.
+    intro H1. rewrite H1. case (MapGet B m' a); reflexivity.
+    exact (H a).
   Qed.
 
-  Lemma MapDisjoint_2_imp : (m:(Map A)) (m':(Map B)) (MapDisjoint_2 m m') -> 
-      (MapDisjoint m m').
+  Lemma MapDisjoint_2_imp :
+   forall (m:Map A) (m':Map B), MapDisjoint_2 m m' -> MapDisjoint m m'.
   Proof.
-    Unfold MapDisjoint MapDisjoint_2. Unfold eqmap eqm. Intros. Elim (in_dom_some ? ? ? H0).
-    Intros y H2. Elim (in_dom_some ? ? ? H1). Intros y' H3.
-    Cut (MapGet A (MapDomRestrTo A B m m') a)=(NONE A). Intro.
-    Rewrite (MapDomRestrTo_semantics ? ? m m' a) in H4. Rewrite H3 in H4. Rewrite H2 in H4.
-    Discriminate H4.
-    Exact (H a).
+    unfold MapDisjoint, MapDisjoint_2 in |- *. unfold eqmap, eqm in |- *. intros. elim (in_dom_some _ _ _ H0).
+    intros y H2. elim (in_dom_some _ _ _ H1). intros y' H3.
+    cut (MapGet A (MapDomRestrTo A B m m') a = NONE A). intro.
+    rewrite (MapDomRestrTo_semantics _ _ m m' a) in H4. rewrite H3 in H4. rewrite H2 in H4.
+    discriminate H4.
+    exact (H a).
   Qed.
 
-  Lemma Map_M0_disjoint : (m:(Map B)) (MapDisjoint (M0 A) m).
+  Lemma Map_M0_disjoint : forall m:Map B, MapDisjoint (M0 A) m.
   Proof.
-    Unfold MapDisjoint in_dom. Intros. Discriminate H.
+    unfold MapDisjoint, in_dom in |- *. intros. discriminate H.
   Qed.
 
-  Lemma Map_disjoint_M0 : (m:(Map A)) (MapDisjoint m (M0 B)).
+  Lemma Map_disjoint_M0 : forall m:Map A, MapDisjoint m (M0 B).
   Proof.
-    Unfold MapDisjoint in_dom. Intros. Discriminate H0.
+    unfold MapDisjoint, in_dom in |- *. intros. discriminate H0.
   Qed.
 
 End MapDisjointDef.
 
 Section MapDisjointExtra.
 
-  Variable A, B : Set.
+  Variables A B : Set.
 
-  Lemma MapDisjoint_ext : (m0,m1:(Map A)) (m2,m3:(Map B))
-      (eqmap A m0 m1) -> (eqmap B m2 m3) -> 
-        (MapDisjoint A B m0 m2) -> (MapDisjoint A B m1 m3).
+  Lemma MapDisjoint_ext :
+   forall (m0 m1:Map A) (m2 m3:Map B),
+     eqmap A m0 m1 ->
+     eqmap B m2 m3 -> MapDisjoint A B m0 m2 -> MapDisjoint A B m1 m3.
   Proof.
-    Intros. Apply MapDisjoint_2_imp. Unfold MapDisjoint_2.
-    Apply eqmap_trans with m':=(MapDomRestrTo A B m0 m2). Apply eqmap_sym. Apply MapDomRestrTo_ext.
-    Assumption.
-    Assumption.
-    Exact (MapDisjoint_imp_2 ? ? ? ? H1).
+    intros. apply MapDisjoint_2_imp. unfold MapDisjoint_2 in |- *.
+    apply eqmap_trans with (m' := MapDomRestrTo A B m0 m2). apply eqmap_sym. apply MapDomRestrTo_ext.
+    assumption.
+    assumption.
+    exact (MapDisjoint_imp_2 _ _ _ _ H1).
   Qed.
 
-  Lemma MapMerge_disjoint : (m,m':(Map A)) (MapDisjoint A A m m') ->
-      	(a:ad) (in_dom A a (MapMerge A m m'))=
-	       (orb (andb (in_dom A a m) (negb (in_dom A a m')))
-	            (andb (in_dom A a m') (negb (in_dom A a m)))).
+  Lemma MapMerge_disjoint :
+   forall m m':Map A,
+     MapDisjoint A A m m' ->
+     forall a:ad,
+       in_dom A a (MapMerge A m m') =
+       orb (andb (in_dom A a m) (negb (in_dom A a m')))
+         (andb (in_dom A a m') (negb (in_dom A a m))).
   Proof.
-    Unfold MapDisjoint. Intros. Rewrite in_dom_merge. Elim (sumbool_of_bool (in_dom A a m)).
-    Intro H0. Rewrite H0. Elim (sumbool_of_bool (in_dom A a m')). Intro H1. Elim (H a H0 H1).
-    Intro H1. Rewrite H1. Reflexivity.
-    Intro H0. Rewrite H0. Simpl. Rewrite andb_b_true. Reflexivity.
+    unfold MapDisjoint in |- *. intros. rewrite in_dom_merge. elim (sumbool_of_bool (in_dom A a m)).
+    intro H0. rewrite H0. elim (sumbool_of_bool (in_dom A a m')). intro H1. elim (H a H0 H1).
+    intro H1. rewrite H1. reflexivity.
+    intro H0. rewrite H0. simpl in |- *. rewrite andb_b_true. reflexivity.
   Qed.
 
-  Lemma MapDisjoint_M2_l : (m0,m1:(Map A)) (m2,m3:(Map B))
-      (MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3)) -> (MapDisjoint A B m0 m2).
+  Lemma MapDisjoint_M2_l :
+   forall (m0 m1:Map A) (m2 m3:Map B),
+     MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3) -> MapDisjoint A B m0 m2.
   Proof.
-    Unfold MapDisjoint in_dom. Intros. Elim (option_sum ? (MapGet A m0 a)). Intro H2.
-    Elim H2. Intros y H3. Elim (option_sum ? (MapGet B m2 a)). Intro H4. Elim H4.
-    Intros y' H5. Apply (H (ad_double a)).
-    Rewrite (MapGet_M2_bit_0_0 ? (ad_double a) (ad_double_bit_0 a) m0 m1).
-    Rewrite (ad_double_div_2 a). Rewrite H3. Reflexivity.
-    Rewrite (MapGet_M2_bit_0_0 ? (ad_double a) (ad_double_bit_0 a) m2 m3).
-    Rewrite (ad_double_div_2 a). Rewrite H5. Reflexivity.
-    Intro H4. Rewrite H4 in H1. Discriminate H1.
-    Intro H2. Rewrite H2 in H0. Discriminate H0.
+    unfold MapDisjoint, in_dom in |- *. intros. elim (option_sum _ (MapGet A m0 a)). intro H2.
+    elim H2. intros y H3. elim (option_sum _ (MapGet B m2 a)). intro H4. elim H4.
+    intros y' H5. apply (H (ad_double a)).
+    rewrite (MapGet_M2_bit_0_0 _ (ad_double a) (ad_double_bit_0 a) m0 m1).
+    rewrite (ad_double_div_2 a). rewrite H3. reflexivity.
+    rewrite (MapGet_M2_bit_0_0 _ (ad_double a) (ad_double_bit_0 a) m2 m3).
+    rewrite (ad_double_div_2 a). rewrite H5. reflexivity.
+    intro H4. rewrite H4 in H1. discriminate H1.
+    intro H2. rewrite H2 in H0. discriminate H0.
   Qed.
 
-  Lemma MapDisjoint_M2_r : (m0,m1:(Map A)) (m2,m3:(Map B))
-      (MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3)) -> (MapDisjoint A B m1 m3).
+  Lemma MapDisjoint_M2_r :
+   forall (m0 m1:Map A) (m2 m3:Map B),
+     MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3) -> MapDisjoint A B m1 m3.
   Proof.
-    Unfold MapDisjoint in_dom. Intros. Elim (option_sum ? (MapGet A m1 a)). Intro H2.
-    Elim H2. Intros y H3. Elim (option_sum ? (MapGet B m3 a)). Intro H4. Elim H4.
-    Intros y' H5. Apply (H (ad_double_plus_un a)).
-    Rewrite (MapGet_M2_bit_0_1 ? (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) m0 m1).
-    Rewrite (ad_double_plus_un_div_2 a). Rewrite H3. Reflexivity.
-    Rewrite (MapGet_M2_bit_0_1 ? (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) m2 m3).
-    Rewrite (ad_double_plus_un_div_2 a). Rewrite H5. Reflexivity.
-    Intro H4. Rewrite H4 in H1. Discriminate H1.
-    Intro H2. Rewrite H2 in H0. Discriminate H0.
+    unfold MapDisjoint, in_dom in |- *. intros. elim (option_sum _ (MapGet A m1 a)). intro H2.
+    elim H2. intros y H3. elim (option_sum _ (MapGet B m3 a)). intro H4. elim H4.
+    intros y' H5. apply (H (ad_double_plus_un a)).
+    rewrite
+     (MapGet_M2_bit_0_1 _ (ad_double_plus_un a) (ad_double_plus_un_bit_0 a)
+        m0 m1).
+    rewrite (ad_double_plus_un_div_2 a). rewrite H3. reflexivity.
+    rewrite
+     (MapGet_M2_bit_0_1 _ (ad_double_plus_un a) (ad_double_plus_un_bit_0 a)
+        m2 m3).
+    rewrite (ad_double_plus_un_div_2 a). rewrite H5. reflexivity.
+    intro H4. rewrite H4 in H1. discriminate H1.
+    intro H2. rewrite H2 in H0. discriminate H0.
   Qed.
 
-  Lemma MapDisjoint_M2 : (m0,m1:(Map A)) (m2,m3:(Map B))
-      (MapDisjoint A B m0 m2) -> (MapDisjoint A B m1 m3) ->
-      	(MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3)).
+  Lemma MapDisjoint_M2 :
+   forall (m0 m1:Map A) (m2 m3:Map B),
+     MapDisjoint A B m0 m2 ->
+     MapDisjoint A B m1 m3 -> MapDisjoint A B (M2 A m0 m1) (M2 B m2 m3).
   Proof.
-    Unfold MapDisjoint in_dom. Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H3.
-    Rewrite (MapGet_M2_bit_0_1 A a H3 m0 m1) in H1.
-    Rewrite (MapGet_M2_bit_0_1 B a H3 m2 m3) in H2. Exact (H0 (ad_div_2 a) H1 H2).
-    Intro H3. Rewrite (MapGet_M2_bit_0_0 A a H3 m0 m1) in H1.
-    Rewrite (MapGet_M2_bit_0_0 B a H3 m2 m3) in H2. Exact (H (ad_div_2 a) H1 H2).
+    unfold MapDisjoint, in_dom in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H3.
+    rewrite (MapGet_M2_bit_0_1 A a H3 m0 m1) in H1.
+    rewrite (MapGet_M2_bit_0_1 B a H3 m2 m3) in H2. exact (H0 (ad_div_2 a) H1 H2).
+    intro H3. rewrite (MapGet_M2_bit_0_0 A a H3 m0 m1) in H1.
+    rewrite (MapGet_M2_bit_0_0 B a H3 m2 m3) in H2. exact (H (ad_div_2 a) H1 H2).
   Qed.
 
-  Lemma MapDisjoint_M1_l : (m:(Map A)) (a:ad) (y:B)
-      (MapDisjoint B A (M1 B a y) m) -> (in_dom A a m)=false.
+  Lemma MapDisjoint_M1_l :
+   forall (m:Map A) (a:ad) (y:B),
+     MapDisjoint B A (M1 B a y) m -> in_dom A a m = false.
   Proof.
-    Unfold MapDisjoint. Intros. Elim (sumbool_of_bool (in_dom A a m)). Intro H0.
-    Elim (H a (in_dom_M1_1 B a y) H0).
-    Trivial.
+    unfold MapDisjoint in |- *. intros. elim (sumbool_of_bool (in_dom A a m)). intro H0.
+    elim (H a (in_dom_M1_1 B a y) H0).
+    trivial.
   Qed.
 
-  Lemma MapDisjoint_M1_r : (m:(Map A)) (a:ad) (y:B)
-      (MapDisjoint A B m (M1 B a y)) -> (in_dom A a m)=false.
+  Lemma MapDisjoint_M1_r :
+   forall (m:Map A) (a:ad) (y:B),
+     MapDisjoint A B m (M1 B a y) -> in_dom A a m = false.
   Proof.
-    Unfold MapDisjoint. Intros. Elim (sumbool_of_bool (in_dom A a m)). Intro H0.
-    Elim (H a H0 (in_dom_M1_1 B a y)).
-    Trivial.
+    unfold MapDisjoint in |- *. intros. elim (sumbool_of_bool (in_dom A a m)). intro H0.
+    elim (H a H0 (in_dom_M1_1 B a y)).
+    trivial.
   Qed.
 
-  Lemma MapDisjoint_M1_conv_l : (m:(Map A)) (a:ad) (y:B)
-      (in_dom A a m)=false -> (MapDisjoint B A (M1 B a y) m).
+  Lemma MapDisjoint_M1_conv_l :
+   forall (m:Map A) (a:ad) (y:B),
+     in_dom A a m = false -> MapDisjoint B A (M1 B a y) m.
   Proof.
-    Unfold MapDisjoint. Intros. Rewrite (in_dom_M1_2 B a a0 y H0) in H. Rewrite H1 in H.
-    Discriminate H.
+    unfold MapDisjoint in |- *. intros. rewrite (in_dom_M1_2 B a a0 y H0) in H. rewrite H1 in H.
+    discriminate H.
   Qed.
 
-  Lemma MapDisjoint_M1_conv_r : (m:(Map A)) (a:ad) (y:B)
-      (in_dom A a m)=false -> (MapDisjoint A B m (M1 B a y)).
+  Lemma MapDisjoint_M1_conv_r :
+   forall (m:Map A) (a:ad) (y:B),
+     in_dom A a m = false -> MapDisjoint A B m (M1 B a y).
   Proof.
-    Unfold MapDisjoint. Intros. Rewrite (in_dom_M1_2 B a a0 y H1) in H. Rewrite H0 in H.
-    Discriminate H.
+    unfold MapDisjoint in |- *. intros. rewrite (in_dom_M1_2 B a a0 y H1) in H. rewrite H0 in H.
+    discriminate H.
   Qed.
  
-  Lemma MapDisjoint_sym : (m:(Map A)) (m':(Map B))
-      (MapDisjoint A B m m') -> (MapDisjoint B A m' m).
+  Lemma MapDisjoint_sym :
+   forall (m:Map A) (m':Map B), MapDisjoint A B m m' -> MapDisjoint B A m' m.
   Proof.
-    Unfold MapDisjoint. Intros. Exact (H ? H1 H0).
+    unfold MapDisjoint in |- *. intros. exact (H _ H1 H0).
   Qed.
 
-  Lemma MapDisjoint_empty : (m:(Map A)) (MapDisjoint A A m m) -> (eqmap A m (M0 A)).
+  Lemma MapDisjoint_empty :
+   forall m:Map A, MapDisjoint A A m m -> eqmap A m (M0 A).
   Proof.
-    Unfold eqmap eqm. Intros. Rewrite <- (MapDomRestrTo_idempotent A m a).
-    Exact (MapDisjoint_imp_2 A A m m H a).
+    unfold eqmap, eqm in |- *. intros. rewrite <- (MapDomRestrTo_idempotent A m a).
+    exact (MapDisjoint_imp_2 A A m m H a).
   Qed.
 
-  Lemma MapDelta_disjoint : (m,m':(Map A)) (MapDisjoint A A m m') ->
-      (eqmap A (MapDelta A m m') (MapMerge A m m')).
+  Lemma MapDelta_disjoint :
+   forall m m':Map A,
+     MapDisjoint A A m m' -> eqmap A (MapDelta A m m') (MapMerge A m m').
   Proof.
-    Intros.
-    Apply eqmap_trans with m':=(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).
-    Apply MapDelta_as_DomRestrBy.
-    Apply eqmap_trans with m':=(MapDomRestrBy A A (MapMerge A m m') (M0 A)).
-    Apply MapDomRestrBy_ext. Apply eqmap_refl.
-    Exact (MapDisjoint_imp_2 A A m m' H).
-    Apply MapDomRestrBy_m_empty.
+    intros.
+    apply eqmap_trans with
+     (m' := MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).
+    apply MapDelta_as_DomRestrBy.
+    apply eqmap_trans with (m' := MapDomRestrBy A A (MapMerge A m m') (M0 A)).
+    apply MapDomRestrBy_ext. apply eqmap_refl.
+    exact (MapDisjoint_imp_2 A A m m' H).
+    apply MapDomRestrBy_m_empty.
   Qed.
 
   Variable C : Set.
 
-  Lemma MapDomRestr_disjoint : (m:(Map A)) (m':(Map B)) (m'':(Map C))
-      (MapDisjoint A B (MapDomRestrTo A C m m'') (MapDomRestrBy B C m' m'')).
+  Lemma MapDomRestr_disjoint :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     MapDisjoint A B (MapDomRestrTo A C m m'') (MapDomRestrBy B C m' m'').
   Proof.
-    Unfold MapDisjoint. Intros m m' m'' a. Rewrite in_dom_restrto. Rewrite in_dom_restrby.
-    Intros. Elim (andb_prop ? ? H). Elim (andb_prop ? ? H0). Intros. Rewrite H4 in H2.
-    Discriminate H2.
+    unfold MapDisjoint in |- *. intros m m' m'' a. rewrite in_dom_restrto. rewrite in_dom_restrby.
+    intros. elim (andb_prop _ _ H). elim (andb_prop _ _ H0). intros. rewrite H4 in H2.
+    discriminate H2.
   Qed.
 
-  Lemma MapDelta_RestrTo_disjoint : (m,m':(Map A))
-      (MapDisjoint A A (MapDelta A m m') (MapDomRestrTo A A m m')).
+  Lemma MapDelta_RestrTo_disjoint :
+   forall m m':Map A,
+     MapDisjoint A A (MapDelta A m m') (MapDomRestrTo A A m m').
   Proof.
-    Unfold MapDisjoint. Intros m m' a. Rewrite in_dom_delta. Rewrite in_dom_restrto.
-    Intros. Elim (andb_prop ? ? H0). Intros. Rewrite H1 in H. Rewrite H2 in H. Discriminate H.
+    unfold MapDisjoint in |- *. intros m m' a. rewrite in_dom_delta. rewrite in_dom_restrto.
+    intros. elim (andb_prop _ _ H0). intros. rewrite H1 in H. rewrite H2 in H. discriminate H.
   Qed.
 
-  Lemma MapDelta_RestrTo_disjoint_2 : (m,m':(Map A))
-      (MapDisjoint A A (MapDelta A m m') (MapDomRestrTo A A m' m)).
+  Lemma MapDelta_RestrTo_disjoint_2 :
+   forall m m':Map A,
+     MapDisjoint A A (MapDelta A m m') (MapDomRestrTo A A m' m).
   Proof.
-    Unfold MapDisjoint. Intros m m' a. Rewrite in_dom_delta. Rewrite in_dom_restrto.
-    Intros. Elim (andb_prop ? ? H0). Intros. Rewrite H1 in H. Rewrite H2 in H. Discriminate H.
+    unfold MapDisjoint in |- *. intros m m' a. rewrite in_dom_delta. rewrite in_dom_restrto.
+    intros. elim (andb_prop _ _ H0). intros. rewrite H1 in H. rewrite H2 in H. discriminate H.
   Qed.
 
   Variable D : Set.
 
-  Lemma MapSubset_Disjoint : (m:(Map A)) (m':(Map B)) (m'':(Map C)) (m''':(Map D))
-      (MapSubset ? ? m m') -> (MapSubset ? ? m'' m''') -> (MapDisjoint ? ? m' m''') ->
-        (MapDisjoint ? ? m m'').
+  Lemma MapSubset_Disjoint :
+   forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D),
+     MapSubset _ _ m m' ->
+     MapSubset _ _ m'' m''' ->
+     MapDisjoint _ _ m' m''' -> MapDisjoint _ _ m m''.
   Proof.
-    Unfold MapSubset MapDisjoint. Intros. Exact (H1 ? (H ? H2) (H0 ? H3)).
+    unfold MapSubset, MapDisjoint in |- *. intros. exact (H1 _ (H _ H2) (H0 _ H3)).
   Qed.
 
-  Lemma MapSubset_Disjoint_l : (m:(Map A)) (m':(Map B)) (m'':(Map C))
-      (MapSubset ? ? m m') -> (MapDisjoint ? ? m' m'') ->
-        (MapDisjoint ? ? m m'').
+  Lemma MapSubset_Disjoint_l :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     MapSubset _ _ m m' -> MapDisjoint _ _ m' m'' -> MapDisjoint _ _ m m''.
   Proof.
-    Unfold MapSubset MapDisjoint. Intros. Exact (H0 ? (H ? H1) H2).
+    unfold MapSubset, MapDisjoint in |- *. intros. exact (H0 _ (H _ H1) H2).
   Qed.
 
-  Lemma MapSubset_Disjoint_r : (m:(Map A)) (m'':(Map C)) (m''':(Map D))
-      (MapSubset ? ? m'' m''') -> (MapDisjoint ? ? m m''') ->
-        (MapDisjoint ? ? m m'').
+  Lemma MapSubset_Disjoint_r :
+   forall (m:Map A) (m'':Map C) (m''':Map D),
+     MapSubset _ _ m'' m''' ->
+     MapDisjoint _ _ m m''' -> MapDisjoint _ _ m m''.
   Proof.
-    Unfold MapSubset MapDisjoint. Intros. Exact (H0 ? H1 (H ? H2)).
+    unfold MapSubset, MapDisjoint in |- *. intros. exact (H0 _ H1 (H _ H2)).
   Qed.
 
-End MapDisjointExtra.
+End MapDisjointExtra.
\ No newline at end of file