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, 379 insertions, 294 deletions

diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v
index b7cede9440..8420ba381a 100644
--- a/theories/IntMap/Mapc.v
+++ b/theories/IntMap/Mapc.v
@@ -7,451 +7,536 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-Require Bool.
-Require Sumbool.
-Require Arith.
-Require ZArith.
-Require Addr.
-Require Adist.
-Require Addec.
-Require Map.
-Require Mapaxioms.
-Require Fset.
-Require Mapiter.
-Require Mapsubset.
-Require PolyList.
-Require Lsort.
-Require Mapcard.
-Require Mapcanon.
+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 Fset.
+Require Import Mapiter.
+Require Import Mapsubset.
+Require Import List.
+Require Import Lsort.
+Require Import Mapcard.
+Require Import Mapcanon.
 
 Section MapC.
 
-  Variable A, B, C : Set.
+  Variables A B C : Set.
 
-  Lemma MapPut_as_Merge_c : (m:(Map A)) (mapcanon A m) ->
-      (a:ad) (y:A) (MapPut A m a y)=(MapMerge A m (M1 A a y)).
+  Lemma MapPut_as_Merge_c :
+   forall m:Map A,
+     mapcanon A m ->
+     forall (a:ad) (y:A), MapPut A m a y = MapMerge A m (M1 A a y).
   Proof.
-    Intros. Apply mapcanon_unique. Exact (MapPut_canon A m H a y).
-    Apply MapMerge_canon. Assumption.
-    Apply M1_canon.
-    Apply MapPut_as_Merge.
+    intros. apply mapcanon_unique. exact (MapPut_canon A m H a y).
+    apply MapMerge_canon. assumption.
+    apply M1_canon.
+    apply MapPut_as_Merge.
   Qed.
 
-  Lemma MapPut_behind_as_Merge_c : (m:(Map A)) (mapcanon A m) ->
-      (a:ad) (y:A) (MapPut_behind A m a y)=(MapMerge A (M1 A a y) m).
+  Lemma MapPut_behind_as_Merge_c :
+   forall m:Map A,
+     mapcanon A m ->
+     forall (a:ad) (y:A), MapPut_behind A m a y = MapMerge A (M1 A a y) m.
   Proof.
-    Intros. Apply mapcanon_unique. Exact (MapPut_behind_canon A m H a y).
-    Apply MapMerge_canon. Apply M1_canon.
-    Assumption.
-    Apply MapPut_behind_as_Merge.
+    intros. apply mapcanon_unique. exact (MapPut_behind_canon A m H a y).
+    apply MapMerge_canon. apply M1_canon.
+    assumption.
+    apply MapPut_behind_as_Merge.
   Qed.
 
-  Lemma MapMerge_empty_m_c : (m:(Map A)) (MapMerge A (M0 A) m)=m.
+  Lemma MapMerge_empty_m_c : forall m:Map A, MapMerge A (M0 A) m = m.
   Proof.
-    Trivial.
+    trivial.
   Qed.
 
-  Lemma MapMerge_assoc_c : (m,m',m'':(Map A))
-      (mapcanon A m) -> (mapcanon A m') -> (mapcanon A m'') ->
-        (MapMerge A (MapMerge A m m') m'')=(MapMerge A m (MapMerge A m' m'')).
+  Lemma MapMerge_assoc_c :
+   forall m m' m'':Map A,
+     mapcanon A m ->
+     mapcanon A m' ->
+     mapcanon A m'' ->
+     MapMerge A (MapMerge A m m') m'' = MapMerge A m (MapMerge A m' m'').
   Proof.
-    Intros. Apply mapcanon_unique.
-    (Apply MapMerge_canon; Try Assumption). (Apply MapMerge_canon; Try Assumption).
-    (Apply MapMerge_canon; Try Assumption). (Apply MapMerge_canon; Try Assumption).
-    Apply MapMerge_assoc.
+    intros. apply mapcanon_unique.
+    apply MapMerge_canon; try assumption. apply MapMerge_canon; try assumption.
+    apply MapMerge_canon; try assumption. apply MapMerge_canon; try assumption.
+    apply MapMerge_assoc.
   Qed.
 
-  Lemma MapMerge_idempotent_c : (m:(Map A)) (mapcanon A m) -> (MapMerge A m m)=m.
+  Lemma MapMerge_idempotent_c :
+   forall m:Map A, mapcanon A m -> MapMerge A m m = m.
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapMerge_canon; Assumption).
-    Assumption.
-    Apply MapMerge_idempotent.
+    intros. apply mapcanon_unique. apply MapMerge_canon; assumption.
+    assumption.
+    apply MapMerge_idempotent.
   Qed.
 
-  Lemma MapMerge_RestrTo_l_c : (m,m',m'':(Map A)) 
-      (mapcanon A m) -> (mapcanon A m'') -> 
-        (MapMerge A (MapDomRestrTo A A m m') m'')=
-        (MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'')).
+  Lemma MapMerge_RestrTo_l_c :
+   forall m m' m'':Map A,
+     mapcanon A m ->
+     mapcanon A m'' ->
+     MapMerge A (MapDomRestrTo A A m m') m'' =
+     MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapMerge_canon. Apply MapDomRestrTo_canon; Assumption.
-    Assumption.
-    Apply MapDomRestrTo_canon; Apply MapMerge_canon; Assumption.
-    Apply MapMerge_RestrTo_l.
+    intros. apply mapcanon_unique. apply MapMerge_canon. apply MapDomRestrTo_canon; assumption.
+    assumption.
+    apply MapDomRestrTo_canon; apply MapMerge_canon; assumption.
+    apply MapMerge_RestrTo_l.
   Qed.
 
-  Lemma MapRemove_as_RestrBy_c : (m:(Map A)) (mapcanon A m) ->
-      (a:ad) (y:B) (MapRemove A m a)=(MapDomRestrBy A B m (M1 B a y)).
+  Lemma MapRemove_as_RestrBy_c :
+   forall m:Map A,
+     mapcanon A m ->
+     forall (a:ad) (y:B), MapRemove A m a = MapDomRestrBy A B m (M1 B a y).
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapRemove_canon; Assumption).
-    (Apply MapDomRestrBy_canon; Assumption).
-    Apply MapRemove_as_RestrBy.
+    intros. apply mapcanon_unique. apply MapRemove_canon; assumption.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapRemove_as_RestrBy.
   Qed.
 
-  Lemma MapDomRestrTo_assoc_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
-      (mapcanon A m) ->
-        (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')=
-        (MapDomRestrTo A B m (MapDomRestrTo B C m' m'')).
+  Lemma MapDomRestrTo_assoc_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrTo A C (MapDomRestrTo A B m m') m'' =
+     MapDomRestrTo A B m (MapDomRestrTo B C m' m'').
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Try Assumption).
-    (Apply MapDomRestrTo_canon; Try Assumption).
-    (Apply MapDomRestrTo_canon; Try Assumption).
-    Apply MapDomRestrTo_assoc.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon; try assumption.
+    apply MapDomRestrTo_canon; try assumption.
+    apply MapDomRestrTo_canon; try assumption.
+    apply MapDomRestrTo_assoc.
   Qed.
 
-  Lemma MapDomRestrTo_idempotent_c : (m:(Map A)) (mapcanon A m) -> 
-      (MapDomRestrTo A A m m)=m.
+  Lemma MapDomRestrTo_idempotent_c :
+   forall m:Map A, mapcanon A m -> MapDomRestrTo A A m m = m.
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Assumption).
-    Assumption.
-    Apply MapDomRestrTo_idempotent.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon; assumption.
+    assumption.
+    apply MapDomRestrTo_idempotent.
   Qed.
 
-  Lemma MapDomRestrTo_Dom_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
-      (MapDomRestrTo A B m m')=(MapDomRestrTo A unit m (MapDom B m')).
+  Lemma MapDomRestrTo_Dom_c :
+   forall (m:Map A) (m':Map B),
+     mapcanon A m ->
+     MapDomRestrTo A B m m' = MapDomRestrTo A unit m (MapDom B m').
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Assumption).
-    (Apply MapDomRestrTo_canon; Assumption).
-    Apply MapDomRestrTo_Dom.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_Dom.
   Qed.
 
-  Lemma MapDomRestrBy_Dom_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
-      (MapDomRestrBy A B m m')=(MapDomRestrBy A unit m (MapDom B m')).
+  Lemma MapDomRestrBy_Dom_c :
+   forall (m:Map A) (m':Map B),
+     mapcanon A m ->
+     MapDomRestrBy A B m m' = MapDomRestrBy A unit m (MapDom B m').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon; Assumption.
-    Apply MapDomRestrBy_canon; Assumption.
-    Apply MapDomRestrBy_Dom.
+    intros. apply mapcanon_unique. apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_Dom.
   Qed.
 
-  Lemma MapDomRestrBy_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map B)) 
-      (mapcanon A m) -> 
-        (MapDomRestrBy A B (MapDomRestrBy A B m m') m'')=
-        (MapDomRestrBy A B m (MapMerge B m' m'')).
+  Lemma MapDomRestrBy_By_c :
+   forall (m:Map A) (m' m'':Map B),
+     mapcanon A m ->
+     MapDomRestrBy A B (MapDomRestrBy A B m m') m'' =
+     MapDomRestrBy A B m (MapMerge B m' m'').
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDomRestrBy_canon; Try Assumption).
-    (Apply MapDomRestrBy_canon; Try Assumption).
-    (Apply MapDomRestrBy_canon; Try Assumption).
-    Apply MapDomRestrBy_By.
+    intros. apply mapcanon_unique. apply MapDomRestrBy_canon; try assumption.
+    apply MapDomRestrBy_canon; try assumption.
+    apply MapDomRestrBy_canon; try assumption.
+    apply MapDomRestrBy_By.
   Qed.
 
-  Lemma MapDomRestrBy_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
-      (mapcanon A m) ->
-        (MapDomRestrBy A C (MapDomRestrBy A B m m') m'')=
-        (MapDomRestrBy A B (MapDomRestrBy A C m m'') m').
+  Lemma MapDomRestrBy_By_comm_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrBy A C (MapDomRestrBy A B m m') m'' =
+     MapDomRestrBy A B (MapDomRestrBy A C m m'') m'.
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
-    (Apply MapDomRestrBy_canon; Assumption).
-    Apply MapDomRestrBy_canon. (Apply MapDomRestrBy_canon; Assumption).
-    Apply MapDomRestrBy_By_comm.
+    intros. apply mapcanon_unique. apply MapDomRestrBy_canon.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_canon. apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_By_comm.
   Qed.
 
-  Lemma MapDomRestrBy_To_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
-      (mapcanon A m) ->
-        (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
-        (MapDomRestrTo A B m (MapDomRestrBy B C m' m'')).
+  Lemma MapDomRestrBy_To_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrBy A C (MapDomRestrTo A B m m') m'' =
+     MapDomRestrTo A B m (MapDomRestrBy B C m' m'').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
-    (Apply MapDomRestrTo_canon; Assumption).
-    (Apply MapDomRestrTo_canon; Assumption).
-    Apply MapDomRestrBy_To.
+    intros. apply mapcanon_unique. apply MapDomRestrBy_canon.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrBy_To.
   Qed.
 
-  Lemma MapDomRestrBy_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
-      (mapcanon A m) ->
-        (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
-        (MapDomRestrTo A B (MapDomRestrBy A C m m'') m').
+  Lemma MapDomRestrBy_To_comm_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrBy A C (MapDomRestrTo A B m m') m'' =
+     MapDomRestrTo A B (MapDomRestrBy A C m m'') m'.
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
-    Apply MapDomRestrTo_canon; Assumption.
-    Apply MapDomRestrTo_canon. Apply MapDomRestrBy_canon; Assumption.
-    Apply MapDomRestrBy_To_comm.
+    intros. apply mapcanon_unique. apply MapDomRestrBy_canon.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_canon. apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_To_comm.
   Qed.
 
-  Lemma MapDomRestrTo_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
-      (mapcanon A m) ->
-        (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
-        (MapDomRestrTo A C m (MapDomRestrBy C B m'' m')).
+  Lemma MapDomRestrTo_By_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrTo A C (MapDomRestrBy A B m m') m'' =
+     MapDomRestrTo A C m (MapDomRestrBy C B m'' m').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
-    Apply MapDomRestrBy_canon; Assumption.
-    Apply MapDomRestrTo_canon; Assumption.
-    Apply MapDomRestrTo_By.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_By.
   Qed.
 
-  Lemma MapDomRestrTo_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
-      (mapcanon A m) ->
-        (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
-        (MapDomRestrBy A B (MapDomRestrTo A C m m'') m').
+  Lemma MapDomRestrTo_By_comm_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrTo A C (MapDomRestrBy A B m m') m'' =
+     MapDomRestrBy A B (MapDomRestrTo A C m m'') m'.
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
-    (Apply MapDomRestrBy_canon; Assumption).
-    Apply MapDomRestrBy_canon. (Apply MapDomRestrTo_canon; Assumption).
-    Apply MapDomRestrTo_By_comm.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_canon. apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_By_comm.
   Qed.
 
-  Lemma MapDomRestrTo_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C)) 
-      (mapcanon A m) ->
-        (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')=
-        (MapDomRestrTo A B (MapDomRestrTo A C m m'') m').
+  Lemma MapDomRestrTo_To_comm_c :
+   forall (m:Map A) (m':Map B) (m'':Map C),
+     mapcanon A m ->
+     MapDomRestrTo A C (MapDomRestrTo A B m m') m'' =
+     MapDomRestrTo A B (MapDomRestrTo A C m m'') m'.
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
-    Apply MapDomRestrTo_canon; Assumption.
-    Apply MapDomRestrTo_canon. Apply MapDomRestrTo_canon; Assumption.
-    Apply MapDomRestrTo_To_comm.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_canon. apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_To_comm.
   Qed.
 
-  Lemma MapMerge_DomRestrTo_c : (m,m':(Map A)) (m'':(Map B))
-      (mapcanon A m) -> (mapcanon A m') ->
-        (MapDomRestrTo A B (MapMerge A m m') m'')=
-        (MapMerge A (MapDomRestrTo A B m m'') (MapDomRestrTo A B m' m'')).
+  Lemma MapMerge_DomRestrTo_c :
+   forall (m m':Map A) (m'':Map B),
+     mapcanon A m ->
+     mapcanon A m' ->
+     MapDomRestrTo A B (MapMerge A m m') m'' =
+     MapMerge A (MapDomRestrTo A B m m'') (MapDomRestrTo A B m' m'').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
-    (Apply MapMerge_canon; Assumption).
-    Apply MapMerge_canon. (Apply MapDomRestrTo_canon; Assumption).
-    (Apply MapDomRestrTo_canon; Assumption).
-    Apply MapMerge_DomRestrTo.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon.
+    apply MapMerge_canon; assumption.
+    apply MapMerge_canon. apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapMerge_DomRestrTo.
   Qed.
 
-  Lemma MapMerge_DomRestrBy_c : (m,m':(Map A)) (m'':(Map B))
-      (mapcanon A m) -> (mapcanon A m') ->
-        (MapDomRestrBy A B (MapMerge A m m') m'')=
-        (MapMerge A (MapDomRestrBy A B m m'') (MapDomRestrBy A B m' m'')).
+  Lemma MapMerge_DomRestrBy_c :
+   forall (m m':Map A) (m'':Map B),
+     mapcanon A m ->
+     mapcanon A m' ->
+     MapDomRestrBy A B (MapMerge A m m') m'' =
+     MapMerge A (MapDomRestrBy A B m m'') (MapDomRestrBy A B m' m'').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon. Apply MapMerge_canon; Assumption.
-    Apply MapMerge_canon. Apply MapDomRestrBy_canon; Assumption.
-    Apply MapDomRestrBy_canon; Assumption.
-    Apply MapMerge_DomRestrBy.
+    intros. apply mapcanon_unique. apply MapDomRestrBy_canon. apply MapMerge_canon; assumption.
+    apply MapMerge_canon. apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapMerge_DomRestrBy.
   Qed.
 
-  Lemma MapDelta_nilpotent_c : (m:(Map A)) (mapcanon A m) -> 
-      (MapDelta A m m)=(M0 A).
+  Lemma MapDelta_nilpotent_c :
+   forall m:Map A, mapcanon A m -> MapDelta A m m = M0 A.
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
-    Apply M0_canon.
-    Apply MapDelta_nilpotent.
+    intros. apply mapcanon_unique. apply MapDelta_canon; assumption.
+    apply M0_canon.
+    apply MapDelta_nilpotent.
   Qed.
 
-  Lemma MapDelta_as_Merge_c : (m,m':(Map A))
-      (mapcanon A m) -> (mapcanon A m') ->
-        (MapDelta A m m')=
-	(MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m)).
+  Lemma MapDelta_as_Merge_c :
+   forall m m':Map A,
+     mapcanon A m ->
+     mapcanon A m' ->
+     MapDelta A m m' =
+     MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m).
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
-    (Apply MapMerge_canon; Apply MapDomRestrBy_canon; Assumption).
-    Apply MapDelta_as_Merge.
+    intros. apply mapcanon_unique. apply MapDelta_canon; assumption.
+    apply MapMerge_canon; apply MapDomRestrBy_canon; assumption.
+    apply MapDelta_as_Merge.
   Qed.
 
-  Lemma MapDelta_as_DomRestrBy_c : (m,m':(Map A))
-      (mapcanon A m) -> (mapcanon A m') ->
-        (MapDelta A m m')=
-	(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).
+  Lemma MapDelta_as_DomRestrBy_c :
+   forall m m':Map A,
+     mapcanon A m ->
+     mapcanon A m' ->
+     MapDelta A m m' =
+     MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m').
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDelta_canon; Assumption.
-    Apply MapDomRestrBy_canon. (Apply MapMerge_canon; Assumption).
-    Apply MapDelta_as_DomRestrBy.
+    intros. apply mapcanon_unique. apply MapDelta_canon; assumption.
+    apply MapDomRestrBy_canon. apply MapMerge_canon; assumption.
+    apply MapDelta_as_DomRestrBy.
   Qed.
 
-  Lemma MapDelta_as_DomRestrBy_2_c : (m,m':(Map A))
-      (mapcanon A m) -> (mapcanon A m') ->
-        (MapDelta A m m')=
-	(MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m)).
+  Lemma MapDelta_as_DomRestrBy_2_c :
+   forall m m':Map A,
+     mapcanon A m ->
+     mapcanon A m' ->
+     MapDelta A m m' =
+     MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m).
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
-    Apply MapDomRestrBy_canon. Apply MapMerge_canon; Assumption.
-    Apply MapDelta_as_DomRestrBy_2.
+    intros. apply mapcanon_unique. apply MapDelta_canon; assumption.
+    apply MapDomRestrBy_canon. apply MapMerge_canon; assumption.
+    apply MapDelta_as_DomRestrBy_2.
   Qed.
 
-  Lemma MapDelta_sym_c : (m,m':(Map A))
-      (mapcanon A m) -> (mapcanon A m') -> (MapDelta A m m')=(MapDelta A m' m).
+  Lemma MapDelta_sym_c :
+   forall m m':Map A,
+     mapcanon A m -> mapcanon A m' -> MapDelta A m m' = MapDelta A m' m.
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
-    (Apply MapDelta_canon; Assumption). Apply MapDelta_sym.
+    intros. apply mapcanon_unique. apply MapDelta_canon; assumption.
+    apply MapDelta_canon; assumption. apply MapDelta_sym.
   Qed.
 
-  Lemma MapDom_Split_1_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
-      m=(MapMerge A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m')).
+  Lemma MapDom_Split_1_c :
+   forall (m:Map A) (m':Map B),
+     mapcanon A m ->
+     m = MapMerge A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m').
   Proof.
-    Intros. Apply mapcanon_unique. Assumption.
-    Apply MapMerge_canon. Apply MapDomRestrTo_canon; Assumption.
-    Apply MapDomRestrBy_canon; Assumption.
-    Apply MapDom_Split_1.
+    intros. apply mapcanon_unique. assumption.
+    apply MapMerge_canon. apply MapDomRestrTo_canon; assumption.
+    apply MapDomRestrBy_canon; assumption.
+    apply MapDom_Split_1.
   Qed.
 
-  Lemma MapDom_Split_2_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
-      m=(MapMerge A (MapDomRestrBy A B m m') (MapDomRestrTo A B m m')).
+  Lemma MapDom_Split_2_c :
+   forall (m:Map A) (m':Map B),
+     mapcanon A m ->
+     m = MapMerge A (MapDomRestrBy A B m m') (MapDomRestrTo A B m m').
   Proof.
-    Intros. Apply mapcanon_unique. Assumption.
-    Apply MapMerge_canon. (Apply MapDomRestrBy_canon; Assumption).
-    (Apply MapDomRestrTo_canon; Assumption).
-    Apply MapDom_Split_2.
+    intros. apply mapcanon_unique. assumption.
+    apply MapMerge_canon. apply MapDomRestrBy_canon; assumption.
+    apply MapDomRestrTo_canon; assumption.
+    apply MapDom_Split_2.
   Qed.
 
-  Lemma MapDom_Split_3_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
-      (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m'))=
-      (M0 A).
+  Lemma MapDom_Split_3_c :
+   forall (m:Map A) (m':Map B),
+     mapcanon A m ->
+     MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m') =
+     M0 A.
   Proof.
-    Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
-    Apply MapDomRestrTo_canon; Assumption.
-    Apply M0_canon.
-    Apply MapDom_Split_3.
+    intros. apply mapcanon_unique. apply MapDomRestrTo_canon.
+    apply MapDomRestrTo_canon; assumption.
+    apply M0_canon.
+    apply MapDom_Split_3.
   Qed.
 
-  Lemma Map_of_alist_of_Map_c : (m:(Map A)) (mapcanon A m) ->
-      (Map_of_alist A (alist_of_Map A m))=m.
+  Lemma Map_of_alist_of_Map_c :
+   forall m:Map A, mapcanon A m -> Map_of_alist A (alist_of_Map A m) = m.
   Proof.
-    Intros. (Apply mapcanon_unique; Try Assumption). Apply Map_of_alist_canon.
-    Apply Map_of_alist_of_Map.
+    intros. apply mapcanon_unique; try assumption. apply Map_of_alist_canon.
+    apply Map_of_alist_of_Map.
   Qed.
 
-  Lemma alist_of_Map_of_alist_c : (l:(alist A)) (alist_sorted_2 A l) ->
-      (alist_of_Map A (Map_of_alist A l))=l.
+  Lemma alist_of_Map_of_alist_c :
+   forall l:alist A,
+     alist_sorted_2 A l -> alist_of_Map A (Map_of_alist A l) = l.
   Proof.
-    Intros. Apply alist_canonical. Apply alist_of_Map_of_alist.
-    Apply alist_of_Map_sorts2.
-    Assumption.
+    intros. apply alist_canonical. apply alist_of_Map_of_alist.
+    apply alist_of_Map_sorts2.
+    assumption.
   Qed.
 
-  Lemma MapSubset_antisym_c : (m:(Map A)) (m':(Map B))
-      (mapcanon A m) -> (mapcanon B m') ->
-      (MapSubset A B m m') -> (MapSubset B A m' m) -> (MapDom A m)=(MapDom B m').
+  Lemma MapSubset_antisym_c :
+   forall (m:Map A) (m':Map B),
+     mapcanon A m ->
+     mapcanon B m' ->
+     MapSubset A B m m' -> MapSubset B A m' m -> MapDom A m = MapDom B m'.
   Proof.
-    Intros. Apply (mapcanon_unique unit). (Apply MapDom_canon; Assumption).
-    (Apply MapDom_canon; Assumption).
-    (Apply MapSubset_antisym; Assumption).
+    intros. apply (mapcanon_unique unit). apply MapDom_canon; assumption.
+    apply MapDom_canon; assumption.
+    apply MapSubset_antisym; assumption.
   Qed.
 
-  Lemma FSubset_antisym_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      (MapSubset ? ? s s') -> (MapSubset ? ? s' s) -> s=s'.
+  Lemma FSubset_antisym_c :
+   forall s s':FSet,
+     mapcanon unit s ->
+     mapcanon unit s' -> MapSubset _ _ s s' -> MapSubset _ _ s' s -> s = s'.
   Proof.
-    Intros. Apply (mapcanon_unique unit); Try Assumption. Apply FSubset_antisym; Assumption.
+    intros. apply (mapcanon_unique unit); try assumption. apply FSubset_antisym; assumption.
   Qed.
 
-  Lemma MapDisjoint_empty_c : (m:(Map A)) (mapcanon A m) ->
-      (MapDisjoint A A m m) -> m=(M0 A).
+  Lemma MapDisjoint_empty_c :
+   forall m:Map A, mapcanon A m -> MapDisjoint A A m m -> m = M0 A.
   Proof.
-    Intros. Apply mapcanon_unique; Try Assumption; Try Apply M0_canon.
-    Apply MapDisjoint_empty; Assumption.
+    intros. apply mapcanon_unique; try assumption; try apply M0_canon.
+    apply MapDisjoint_empty; assumption.
   Qed.
 
-  Lemma MapDelta_disjoint_c : (m,m':(Map A)) (mapcanon A m) -> (mapcanon A m') ->
-      (MapDisjoint A A m m') -> (MapDelta A m m')=(MapMerge A m m').
+  Lemma MapDelta_disjoint_c :
+   forall m m':Map A,
+     mapcanon A m ->
+     mapcanon A m' ->
+     MapDisjoint A A m m' -> MapDelta A m m' = MapMerge A m m'.
   Proof.
-    Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
-    (Apply MapMerge_canon; Assumption). Apply MapDelta_disjoint; Assumption.
+    intros. apply mapcanon_unique. apply MapDelta_canon; assumption.
+    apply MapMerge_canon; assumption. apply MapDelta_disjoint; assumption.
   Qed.
 
 End MapC.
 
-Lemma FSetDelta_assoc_c : (s,s',s'':FSet)
-    (mapcanon unit s) -> (mapcanon unit s') -> (mapcanon unit s'') ->
-      (MapDelta ? (MapDelta ? s s') s'')=(MapDelta ? s (MapDelta ? s' s'')).
+Lemma FSetDelta_assoc_c :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   mapcanon unit s' ->
+   mapcanon unit s'' ->
+   MapDelta _ (MapDelta _ s s') s'' = MapDelta _ s (MapDelta _ s' s'').
 Proof.
-  Intros. Apply (mapcanon_unique unit). Apply MapDelta_canon. (Apply MapDelta_canon; Assumption).
-  Assumption.
-  Apply MapDelta_canon. Assumption.
-  (Apply MapDelta_canon; Assumption).
-  Apply FSetDelta_assoc; Assumption.
+  intros. apply (mapcanon_unique unit). apply MapDelta_canon. apply MapDelta_canon; assumption.
+  assumption.
+  apply MapDelta_canon. assumption.
+  apply MapDelta_canon; assumption.
+  apply FSetDelta_assoc; assumption.
 Qed.
 
-Lemma FSet_ext_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      ((a:ad) (in_FSet a s)=(in_FSet a s')) -> s=s'.
+Lemma FSet_ext_c :
+ forall s s':FSet,
+   mapcanon unit s ->
+   mapcanon unit s' -> (forall a:ad, in_FSet a s = in_FSet a s') -> s = s'.
 Proof.
-  Intros. (Apply (mapcanon_unique unit); Try Assumption). Apply FSet_ext. Assumption.
+  intros. apply (mapcanon_unique unit); try assumption. apply FSet_ext. assumption.
 Qed.
 
-Lemma FSetUnion_comm_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      (FSetUnion s s')=(FSetUnion s' s).
+Lemma FSetUnion_comm_c :
+ forall s s':FSet,
+   mapcanon unit s -> mapcanon unit s' -> FSetUnion s s' = FSetUnion s' s.
 Proof.
-  Intros.
-  Apply (mapcanon_unique unit); Try (Unfold FSetUnion; Apply MapMerge_canon; Assumption).
-  Apply FSetUnion_comm.
+  intros.
+  apply (mapcanon_unique unit);
+   try (unfold FSetUnion in |- *; apply MapMerge_canon; assumption).
+  apply FSetUnion_comm.
 Qed.
 
-Lemma FSetUnion_assoc_c : (s,s',s'':FSet)
-      (mapcanon unit s) -> (mapcanon unit s') -> (mapcanon unit s'') ->
-        (FSetUnion (FSetUnion s s') s'')=(FSetUnion s (FSetUnion s' s'')).
+Lemma FSetUnion_assoc_c :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   mapcanon unit s' ->
+   mapcanon unit s'' ->
+   FSetUnion (FSetUnion s s') s'' = FSetUnion s (FSetUnion s' s'').
 Proof.
-  Exact (MapMerge_assoc_c unit).
+  exact (MapMerge_assoc_c unit).
 Qed.
 
-Lemma FSetUnion_M0_s_c : (s:FSet) (FSetUnion (M0 unit) s)=s.
+Lemma FSetUnion_M0_s_c : forall s:FSet, FSetUnion (M0 unit) s = s.
 Proof.
-  Exact (MapMerge_empty_m_c unit).
+  exact (MapMerge_empty_m_c unit).
 Qed.
 
-Lemma FSetUnion_s_M0_c : (s:FSet) (FSetUnion s (M0 unit))=s.
+Lemma FSetUnion_s_M0_c : forall s:FSet, FSetUnion s (M0 unit) = s.
 Proof.
-  Exact (MapMerge_m_empty_1 unit).
+  exact (MapMerge_m_empty_1 unit).
 Qed.
 
-Lemma FSetUnion_idempotent : (s:FSet) (mapcanon unit s) -> (FSetUnion s s)=s.
+Lemma FSetUnion_idempotent :
+ forall s:FSet, mapcanon unit s -> FSetUnion s s = s.
 Proof.
-  Exact (MapMerge_idempotent_c unit).
+  exact (MapMerge_idempotent_c unit).
 Qed.
 
-Lemma FSetInter_comm_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      (FSetInter s s')=(FSetInter s' s).
+Lemma FSetInter_comm_c :
+ forall s s':FSet,
+   mapcanon unit s -> mapcanon unit s' -> FSetInter s s' = FSetInter s' s.
 Proof.
-  Intros.
-  Apply (mapcanon_unique unit); Try (Unfold FSetInter; Apply MapDomRestrTo_canon; Assumption).
-  Apply FSetInter_comm.
+  intros.
+  apply (mapcanon_unique unit);
+   try (unfold FSetInter in |- *; apply MapDomRestrTo_canon; assumption).
+  apply FSetInter_comm.
 Qed.
 
-Lemma FSetInter_assoc_c : (s,s',s'':FSet)
-      (mapcanon unit s) ->
-        (FSetInter (FSetInter s s') s'')=(FSetInter s (FSetInter s' s'')).
+Lemma FSetInter_assoc_c :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   FSetInter (FSetInter s s') s'' = FSetInter s (FSetInter s' s'').
 Proof.
-  Exact (MapDomRestrTo_assoc_c unit unit unit).
+  exact (MapDomRestrTo_assoc_c unit unit unit).
 Qed.
 
-Lemma FSetInter_M0_s_c : (s:FSet) (FSetInter (M0 unit) s)=(M0 unit).
+Lemma FSetInter_M0_s_c : forall s:FSet, FSetInter (M0 unit) s = M0 unit.
 Proof.
-  Trivial.
+  trivial.
 Qed.
 
-Lemma FSetInter_s_M0_c : (s:FSet) (FSetInter s (M0 unit))=(M0 unit).
+Lemma FSetInter_s_M0_c : forall s:FSet, FSetInter s (M0 unit) = M0 unit.
 Proof.
-  Exact (MapDomRestrTo_m_empty_1 unit unit).
+  exact (MapDomRestrTo_m_empty_1 unit unit).
 Qed.
 
-Lemma FSetInter_idempotent : (s:FSet) (mapcanon unit s) -> (FSetInter s s)=s.
+Lemma FSetInter_idempotent :
+ forall s:FSet, mapcanon unit s -> FSetInter s s = s.
 Proof.
-  Exact (MapDomRestrTo_idempotent_c unit).
+  exact (MapDomRestrTo_idempotent_c unit).
 Qed.
 
-Lemma FSetUnion_Inter_l_c : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s'') ->
-      (FSetUnion (FSetInter s s') s'')=(FSetInter (FSetUnion s s'') (FSetUnion s' s'')).
+Lemma FSetUnion_Inter_l_c :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   mapcanon unit s'' ->
+   FSetUnion (FSetInter s s') s'' =
+   FSetInter (FSetUnion s s'') (FSetUnion s' s'').
 Proof.
-  Intros. Apply (mapcanon_unique unit). Unfold FSetUnion. (Apply MapMerge_canon; Try Assumption).
-  Unfold FSetInter. (Apply MapDomRestrTo_canon; Assumption).
-  Unfold FSetInter; Unfold FSetUnion; Apply MapDomRestrTo_canon; Apply MapMerge_canon; Assumption.
-  Apply FSetUnion_Inter_l.
+  intros. apply (mapcanon_unique unit). unfold FSetUnion in |- *. apply MapMerge_canon; try assumption.
+  unfold FSetInter in |- *. apply MapDomRestrTo_canon; assumption.
+  unfold FSetInter in |- *; unfold FSetUnion in |- *;
+   apply MapDomRestrTo_canon; apply MapMerge_canon; 
+   assumption.
+  apply FSetUnion_Inter_l.
 Qed.
 
-Lemma FSetUnion_Inter_r : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      (FSetUnion s (FSetInter s' s''))=(FSetInter (FSetUnion s s') (FSetUnion s s'')).
+Lemma FSetUnion_Inter_r :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   mapcanon unit s' ->
+   FSetUnion s (FSetInter s' s'') =
+   FSetInter (FSetUnion s s') (FSetUnion s s'').
 Proof.
-  Intros. Apply (mapcanon_unique unit). Unfold FSetUnion. (Apply MapMerge_canon; Try Assumption).
-  Unfold FSetInter. (Apply MapDomRestrTo_canon; Assumption).
-  Unfold FSetInter; Unfold FSetUnion; Apply MapDomRestrTo_canon; Apply MapMerge_canon; Assumption.
-  Apply FSetUnion_Inter_r.
+  intros. apply (mapcanon_unique unit). unfold FSetUnion in |- *. apply MapMerge_canon; try assumption.
+  unfold FSetInter in |- *. apply MapDomRestrTo_canon; assumption.
+  unfold FSetInter in |- *; unfold FSetUnion in |- *;
+   apply MapDomRestrTo_canon; apply MapMerge_canon; 
+   assumption.
+  apply FSetUnion_Inter_r.
 Qed.
 
-Lemma FSetInter_Union_l_c : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      (FSetInter (FSetUnion s s') s'')=(FSetUnion (FSetInter s s'') (FSetInter s' s'')).
+Lemma FSetInter_Union_l_c :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   mapcanon unit s' ->
+   FSetInter (FSetUnion s s') s'' =
+   FSetUnion (FSetInter s s'') (FSetInter s' s'').
 Proof.
-  Intros. Apply (mapcanon_unique unit). Unfold FSetInter.
-  Apply MapDomRestrTo_canon; Try Assumption. Unfold FSetUnion.
-  Apply MapMerge_canon; Assumption.
-  Unfold FSetUnion; Unfold FSetInter; Apply MapMerge_canon; Apply MapDomRestrTo_canon;
-  Assumption.
-  Apply FSetInter_Union_l.
+  intros. apply (mapcanon_unique unit). unfold FSetInter in |- *.
+  apply MapDomRestrTo_canon; try assumption. unfold FSetUnion in |- *.
+  apply MapMerge_canon; assumption.
+  unfold FSetUnion in |- *; unfold FSetInter in |- *; apply MapMerge_canon;
+   apply MapDomRestrTo_canon; assumption.
+  apply FSetInter_Union_l.
 Qed.
 
-Lemma FSetInter_Union_r : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
-      (FSetInter s (FSetUnion s' s''))=(FSetUnion (FSetInter s s') (FSetInter s s'')).
+Lemma FSetInter_Union_r :
+ forall s s' s'':FSet,
+   mapcanon unit s ->
+   mapcanon unit s' ->
+   FSetInter s (FSetUnion s' s'') =
+   FSetUnion (FSetInter s s') (FSetInter s s'').
 Proof.
-  Intros. Apply (mapcanon_unique unit). Unfold FSetInter.
-  Apply MapDomRestrTo_canon; Try Assumption.
-  Unfold FSetUnion. Apply MapMerge_canon; Unfold FSetInter; Apply MapDomRestrTo_canon; Assumption.
-  Apply FSetInter_Union_r.
-Qed.
+  intros. apply (mapcanon_unique unit). unfold FSetInter in |- *.
+  apply MapDomRestrTo_canon; try assumption.
+  unfold FSetUnion in |- *. apply MapMerge_canon; unfold FSetInter in |- *; apply MapDomRestrTo_canon;
+  assumption.
+  apply FSetInter_Union_r.
+Qed.
\ No newline at end of file