diff --git a/SConstruct b/SConstruct
index 2a03da7..af0a615 100644
--- a/SConstruct
+++ b/SConstruct
@@ -1,12 +1,13 @@
 import os, glob, string
 libs = os.environ["COQLIBS"]
+coqtop = os.environ["COQTOP"]
 corn_dir = libs + '/CoRN'
 color_dir = libs + '/color/color/trunk/color'
 
 Rs = [(corn_dir, 'CoRN'), (color_dir, 'CoLoR'), ('.', 'hybrid')]
 Rs = string.join(map(lambda (x,y): '-R "' + x + '" ' + y, Rs))
 
-coqc = 'coqc -noglob ' + Rs
+coqc = coqtop + '/bin/coqc -noglob ' + Rs
 
 def make_abs(s):
   if s[0] != '/': return Dir("#").abspath + "/" + s
diff --git a/abstract.v b/abstract.v
index 33b982f..8682023 100644
--- a/abstract.v
+++ b/abstract.v
@@ -5,6 +5,10 @@ Require Import Morphisms.
 Set Implicit Arguments.
 Require Import EquivDec.
 Require concrete.
+Require Import CoLoR.Util.Vector.VecUtil.
+Require Import hybrid.vector_setoid.
+Require hybrid.nat_util.
+Require Import hybrid.hlist_aux.
 
 Module c := concrete.
 
@@ -13,7 +17,7 @@ Section contents.
   Variable chs: concrete.System.
 
   Record Space: Type :=
-    { Region: Set
+    { Region: Type
     ; Region_eq_dec: EquivDec.EqDec Region eq
     ; regions: ExhaustiveList Region
     ; NoDup_regions: NoDup regions
@@ -62,23 +66,70 @@ Section contents.
     Let in_region_mor: Morphism (@cs_eq _ ==> eq ==> iff) in_region.
     Proof. unfold in_region. intros x x' e r r' e'. rewrite e, e'. split; auto. Qed.
 
-    Let regions_cover: forall (l : concrete.Location chs) (p : concrete.Point chs),
-      concrete.invariant (l, p) -> DN (sig (in_region p)).
-    Proof.
-      intros.
-      apply (DN_bind (regions_cover ap _ _ H)). intros [x i].
-      apply (DN_bind (regions_cover ap' _ _ H)). intros [x0 i0].
-      apply DN_return.
-      exists (x, x0).
-      split; assumption.
-    Qed. (* written with Program and monad notation, this should be much clearer *)
+    Program Definition regions_cover_prod l p : concrete.invariant (l, p) -> DN (sig (in_region p)) :=
+      fun H => 
+        C1 <- contents.regions_cover ap l p H;
+        C2 <- contents.regions_cover ap' l p H;
+        return [=(`C1, `C2)=].
+    Next Obligation.
+      split; crunch.
+    Qed.
 
     Definition prod_space: Space := Build_Space _ _
       (NoDup_ExhaustivePairList (NoDup_regions ap) (NoDup_regions ap'))
-      in_region_mor regions_cover.
+      in_region_mor regions_cover_prod.
 
   End prod_space.
 
+  (* We generalize the product space above from 2 to arbitrary 'n' dimensions,
+     hence generalizing abstraction by squares in 2 dimensional space to 
+     abstraction by hyper-cubes in n-dimensional space *)
+
+  Section hyper_space.
+
+    Variable n : nat.
+    Variable aps : list Space.
+
+    (* [Regions] is formed by an n-product of [Region]s of respective [Space]s,
+       epxressed with heterogenous list *)
+    Notation Regions aps := (@hlist _ Region aps).
+
+    Fixpoint in_region_aux (aps : list Space) (p : concrete.Point chs) : Regions aps -> Prop :=
+      match aps as aps return Regions aps -> Prop with
+      | [] => fun _ => True
+      | s::ss => fun rs =>
+          in_region s p (hhd rs) /\ @in_region_aux ss p (htl rs)
+      end.
+
+    Obligation Tactic := crunch.
+
+    Program Fixpoint regions_cover_aux (aps : list Space) l p : 
+      concrete.invariant (l, p) -> DN (sig (@in_region_aux aps p)) :=
+      match aps with
+      | [] => fun H => return [= HNil (H:=_) =]
+      | s::ss => fun H =>
+          C1 <- contents.regions_cover s l p H;
+          C2 <- @regions_cover_aux ss l p H;
+          return [= `C1:::`C2 =]
+      end.
+
+    Lemma in_region_aux_morph : Morphism (@st_eq _ ==> eq ==> iff) (@in_region_aux aps).
+    Proof.
+      repeat intro; split; induction aps; crunch.
+    Qed.
+
+    Obligation Tactic := program_simpl; auto with typeclass_instances.
+
+    Hint Resolve NoDup_regions.
+
+    Program Definition hyper_space : Space := @Build_Space (Regions aps) _ _ _ 
+      (@in_region_aux aps) in_region_aux_morph (@regions_cover_aux aps).
+    Next Obligation.
+      set (w := NoDup_ExhaustiveHList); simpl in w; apply w; auto.
+    Qed.
+
+  End hyper_space.
+
   Variable ap: Space.
 
   Instance abs: Container (c.State chs) (State ap) := fun s s' =>
@@ -95,7 +146,7 @@ Section contents.
 
   End CoverRelandsuch.
 
-  Definition CompleteCoverList (cs: c.State chs -> Prop): Set :=
+  Definition CompleteCoverList (cs: c.State chs -> Prop): Type :=
     sig (LazyProp ∘ (CompleteCover cs: list (State ap) -> Prop)).
 
   Section safe.
@@ -145,7 +196,7 @@ Section contents.
   Definition cont_trans (l: c.Location chs): relation (Region ap)
     := fun r r' => exists p q, p ∈ r /\ q ∈ r' /\ c.can_flow chs l p q.
 
-  Definition sharing_transition_overestimator (R: relation (concrete.State chs)): Set :=
+  Definition sharing_transition_overestimator (R: relation (concrete.State chs)): Type :=
     forall s: State ap, sig (fun l: list (State ap) => LazyProp (NoDup l /\
       SharedCover (concrete.invariant ∩ (overlap s ∘ util.flip R)) l)).
         (* the invariant part is important because it means the overestimators can use
diff --git a/abstract_as_graph.v b/abstract_as_graph.v
index 3478ea4..a50a96a 100644
--- a/abstract_as_graph.v
+++ b/abstract_as_graph.v
@@ -14,7 +14,7 @@ Section using_duplication.
     (ap: abstract.Space chs)
     (ahs: abstract.System ap).
 
-  Let Vertex := bool * abstract.State ap.
+  Let Vertex : Type := bool * abstract.State ap.
 
   Definition nexts (v: Vertex): list (abstract.State ap) :=
     let (k, s) := v in
diff --git a/decreasing_exponential_flow.v b/decreasing_exponential_flow.v
index c51ba89..2f7f792 100644
--- a/decreasing_exponential_flow.v
+++ b/decreasing_exponential_flow.v
@@ -474,3 +474,5 @@ Section contents.
   Qed.
 
 End contents.
+
+Hint Resolve inv_correct.
diff --git a/digraph.v b/digraph.v
index 6262c01..c233fea 100644
--- a/digraph.v
+++ b/digraph.v
@@ -4,7 +4,7 @@ Require EquivDec.
 Set Implicit Arguments.
 
 Record DiGraph: Type := Build
-  { Vertex: Set
+  { Vertex: Type
   ; Vertex_eq_dec: EquivDec.EqDec Vertex eq
   ; vertices: ExhaustiveList Vertex
   ; edges: Vertex -> list Vertex
@@ -29,7 +29,7 @@ Section reachability.
   Definition edge: relation (Vertex g) := fun v w => In w (edges v).
   Let ved := Vertex_eq_dec g.
 
-  Definition Edge: Set := (Vertex g * Vertex g)%type.
+  Definition Edge := (Vertex g * Vertex g)%type.
   Definition Edge_eq_dec: forall (e e': Edge), decision (e=e')
     := pair_eq_dec ved ved.
 
diff --git a/examples/room_heating/abs.v b/examples/room_heating/abs.v
new file mode 100644
index 0000000..33511b2
--- /dev/null
+++ b/examples/room_heating/abs.v
@@ -0,0 +1,33 @@
+Require Import hybrid.tactics.
+Require Import hybrid.abstract.
+Require Import hybrid.geometry.
+Require Import hybrid.square_abstraction.
+Require Import hybrid.flow.
+
+Require Import hybrid.examples.room_heating.conc.
+
+Set Implicit Arguments.
+
+Local Open Scope CR_scope.
+Local Open Scope vec_scope.
+
+Module RoomHeatingAbstract (Import RHS : RoomHeatingSpec).
+
+  Module Import conc := RoomHeatingConcrete RHS.
+
+  Definition two_pos: CRpos ('2) := positive_CRpos 2.
+
+  Definition room_flow_inv (rs : RoomState) : OpenRange -> OpenRange -> OpenRange :=
+    match rs with
+    | HeaterOn => flow.scale.inv two_pos (square_flow_conditions.one_axis.flow_range
+      _ flow.positive_linear.inv_correct flow.positive_linear.mono)
+    | HeaterOff
+    | NoHeater => decreasing_exponential_flow.inv milli
+    end.
+
+  Lemma room_flow_ok l : range_flow_inv_spec (room_flow l) (room_flow_inv l).
+  Proof with auto.
+    destruct l; crunch.
+  Qed.
+
+End RoomHeatingAbstract.
diff --git a/examples/room_heating/conc.v b/examples/room_heating/conc.v
index 01808b5..0c10003 100644
--- a/examples/room_heating/conc.v
+++ b/examples/room_heating/conc.v
@@ -3,6 +3,7 @@ Require  Coq.Program.Program.
 Require Import CoRN.reals.fast.CRln.
 
 Require Export hybrid.examples.room_heating.params.
+Require Import hybrid.tactics.
 Require Import hybrid.util.
 Require Import hybrid.c_util.
 Require Import hybrid.nat_util.
@@ -64,7 +65,7 @@ Module RoomHeatingConcrete (Import RHS : RoomHeatingSpec).
   Lemma exhaustiveRS_correct x : In x (exhaustiveRS n).
   Proof with auto.
     induction x.
-    left. ref.
+    crunch.
     simpl. destruct a; in_or_app_proof.
   Qed.
 
@@ -207,7 +208,10 @@ Module RoomHeatingConcrete (Import RHS : RoomHeatingSpec).
   Definition flow (l : DS) := vector_flow (Vmap room_flow l).
 
   Lemma invariant_stable s: Stable (invariant s).
-  Admitted.
+  Proof.
+    intros. apply check_n_Stable.
+    intros. destruct (ds s) [@ip]; crunch.
+  Qed.
 
   Definition concrete_system: concrete.System :=
     concrete.Build_System _ _ NoDup_locations
diff --git a/examples/thermostat/abs.v b/examples/thermostat/abs.v
index a552610..b23f6c2 100644
--- a/examples/thermostat/abs.v
+++ b/examples/thermostat/abs.v
@@ -3,6 +3,7 @@ Require Import geometry.
 Require Import monotonic_flow.
 Require Import hs_solver.
 Require Import interval_spec.
+Require Import tactics.
 Require decreasing_exponential_flow.
 Require abstract square_abstraction.
 Require EquivDec.
@@ -32,22 +33,16 @@ Definition temp_flow_inv (l: Location): OpenRange -> OpenRange -> OpenRange :=
   | Check => flow.scale.inv half_pos (dec_exp_flow.inv milli)
   end.
 
+Hint Resolve square_flow_conditions.one_axis.flow_range_covers.
+
 Lemma clock_rfis l: range_flow_inv_spec (clock_flow l) (clock_flow_inv l).
-Proof with auto.
-  intro.
-  unfold range_flow_inv_spec. intros.
-  apply square_flow_conditions.one_axis.flow_range_covers with p...
+Proof.
+  unfold clock_flow_inv; crunch.
 Qed.
 
 Lemma temp_rfis l: range_flow_inv_spec (temp_flow l) (temp_flow_inv l).
-Proof with auto.
-  destruct l; simpl temp_flow.
-      unfold temp_flow_inv.
-      apply flow.scale.inv_correct.
-      unfold range_flow_inv_spec. intros.
-      apply square_flow_conditions.one_axis.flow_range_covers with p...
-    apply dec_exp_flow.inv_correct.
-  apply flow.scale.inv_correct, dec_exp_flow.inv_correct.
+Proof. 
+  destruct l; crunch.
 Qed.
 
 (* Abstract regions: *)
diff --git a/flow.v b/flow.v
index cdd9d87..600f698 100644
--- a/flow.v
+++ b/flow.v
@@ -22,13 +22,14 @@ Record Flow (X: CSetoid): Type :=
   }.
 
 Definition mono (f: Flow CRasCSetoid): Type :=
-  sum (forall x, strongly_increasing (f x))
-    (forall x, strongly_decreasing (f x)).
+  ((forall x, strongly_increasing (f x)) + (forall x, strongly_decreasing (f x)))%type.
 
 Definition range_flow_inv_spec (f: Flow CRasCSetoid)
   (i: OpenRange -> OpenRange -> OpenRange): Prop :=
     forall a p, in_orange a p -> forall b t, in_orange b (f p t) -> in_orange (i a b) t.
 
+Hint Unfold range_flow_inv_spec.
+
 Obligation Tactic := idtac.
 
 Program Definition product_flow (X Y: CSetoid) (fx: Flow X) (fy: Flow Y):
@@ -149,7 +150,7 @@ Section contents.
 End contents.
 End scale.
 
-Hint Resolve scale.inc.
+Hint Resolve scale.inc scale.inv_correct.
 
 Module positive_linear.
 Section contents.
diff --git a/hlist.v b/hlist.v
new file mode 100644
index 0000000..2019928
--- /dev/null
+++ b/hlist.v
@@ -0,0 +1,268 @@
+Require Export hybrid.tactics.
+Require Export hybrid.util.
+Require Import hybrid.list_util.
+Require Export Coq.Lists.List.
+Require Export Coq.Classes.EquivDec.
+Require Import Coq.Logic.Eqdep_dec.
+
+Set Implicit Arguments.
+
+(** * Heterogenous lists *)
+
+Section hlists_def.
+
+  Context `{B : A -> Type}.
+
+  (* heterogenous list parametrized by 'list signature' *)
+  Inductive hlist : list A -> Type :=
+  | HNil : hlist nil
+  | HCons : forall x xs, B x -> hlist xs -> hlist (x::xs)
+  .
+
+End hlists_def.
+
+Implicit Arguments HNil [A B].
+Implicit Arguments HCons [A B x xs].
+
+Infix ":::" := HCons (right associativity, at level 60).
+
+Ltac hlist_simpl :=
+  repeat 
+    match goal with
+    | hl : hlist [] |- _ => dep_destruct hl
+    | hl : hlist (_::_) |- _ => dep_destruct hl
+    | H : _:::_ = _:::_ |- _ => inversion H; clear H
+    end.
+
+ (** [hget] on [HList]s is similar to [Vnth] on [vector]s *)
+Section hlist_get.
+
+  Context `{B : A -> Type, elt : A}.
+
+  Inductive member : list A -> Type :=
+  | MFirst : forall ls, member (elt :: ls)
+  | MNext : forall x ls, member ls -> member (x::ls)
+  .
+  
+  Fixpoint hget lt (l : hlist lt) : member lt -> B elt :=
+    match l with
+      | HNil => fun p =>
+        match p in member lt 
+          return 
+            match lt with 
+            | nil => B elt
+            | _ => unit 
+            end 
+        with
+        | MFirst _ => tt
+        | MNext _ _ _ => tt
+        end
+      | HCons _ _ x xs => fun p =>
+        match p in member lt
+          return 
+          match lt with
+          | nil => unit
+          | x::lt => B x -> (member lt -> B elt) -> B elt
+          end
+        with
+        | MFirst _ => fun x get_xs => x
+        | MNext _ _ p' => fun _ get_xs => get_xs p'
+        end x (hget xs)
+    end.
+
+End hlist_get.
+
+(** Decidability of Leibniz equality on [HList]s (given deecidable 
+    equality on all types of its elements). *)
+Section hlist_eqdec.
+
+  Context `{B : A -> Type, lt : list A}.
+  Variable EltsEqDec : forall x, In x lt -> EqDec (B x) eq.
+
+  Lemma hlist_eq_fst_eq a lt (x y : B a) (xs ys : hlist lt) :
+    x:::xs === y:::ys ->
+    x === y.
+  Proof.
+    inversion 1; dep_subst; intuition.
+  Qed.
+
+  Lemma hlist_eq_snd_eq a lt (x y : B a) (xs ys : hlist lt) :
+    x:::xs === y:::ys ->
+    xs === ys.
+  Proof.
+    inversion 1; dep_subst; intuition.
+  Qed.
+
+  Global Hint Resolve hlist_eq_fst_eq hlist_eq_snd_eq.
+
+  Global Program Instance hlist_EqDec : EqDec (hlist (B:=B) lt) eq.
+  Next Obligation.
+    revert x y; induction lt; intros; hlist_simpl; crunch;
+      match goal with
+      | EQ : forall x, ?a = x \/ In x ?l -> _, x : B ?a, y : B ?a 
+          |- context [?x:::_ === ?y:::_] =>
+          let a_al0 := fresh "a_al0" in
+          assert (a_al0 : In a (a :: l)) by intuition;
+          destruct (EQ a a_al0 x y)
+      end;
+      match goal with
+      | IH : (forall x, In x ?l -> EqDec (?B x) eq) -> forall x y, {x === y} + {x =/= y} 
+          |- context [_:::?xs === _:::?ys] =>
+          let IHpre := fresh "IHpre" in
+          assert (IHpre : forall x, In x l -> EqDec (B x) eq) by intuition;
+          destruct (IH IHpre xs ys)
+      end;
+      simpl_eqs; crunch; compute; crunch.
+  Qed.
+
+End hlist_eqdec.
+
+Section hlist_funs.
+
+  Variables (A : Type) (B : A -> Type) (lt : list A).
+(* FIXME, using instead the Context below gives a wrong type for hbuild,
+          as [lt] is unneccessarily abstracted in it. This problem with
+          Context is fixed in 8.3 *)
+(*  Context `{B : A -> Type}{lt : list A}.*)
+
+  (** [hsingleton x] is a [HList] with only one element [x] *)
+  Definition hsingleton (t : A) (x : B t) : hlist [t] := x:::HNil.
+
+  (** [hhd] of [x::xs] is [x] *)
+  Definition hhd (l : hlist lt) :=
+    match l in hlist lt
+      return match lt with
+             | nil => unit
+             | x::_ => B x
+             end
+    with
+    | HNil => tt
+    | HCons _ _ x _ => x
+    end.
+
+  (** [htl] of [x::xs] is [xs] *)
+  Definition htl (l : hlist (B:=B) lt) :=
+    match l in hlist lt
+      return match lt with
+             | nil => unit
+             | _ :: lt' => hlist lt'
+             end 
+    with
+    | HNil => tt
+    | HCons _ _ _ tl => tl
+    end.
+
+  (** [happ [x_1; ... x_n] [y_1; ... y_n] = [x_1; ... x_n; y_1; ... y_n]] *)
+  Fixpoint happ (lt1 : list A) (l1 : hlist (B:=B) lt1) : 
+    forall lt2, hlist lt2 -> hlist (lt1 ++ lt2) :=
+    match l1 in hlist lt1 
+      return forall lt2, hlist lt2 -> hlist (lt1 ++ lt2) 
+    with
+    | HNil => fun _ l2 => l2
+    | HCons _ _ x l1' => fun _ l2 => HCons x (happ l1' l2)
+    end.
+
+  Variable f : forall x, B x.
+
+  (** [hbuild [t_1; ... t_n] = [f t_1; ... f t_n]] *)
+  Fixpoint hbuild (lt : list A) : hlist lt :=
+    match lt with
+    | nil => HNil
+    | x::lt' => HCons (f x) (hbuild lt')
+    end.
+
+End hlist_funs.
+
+Infix "+++" := happ (right associativity, at level 60).
+
+Section HList_prods.
+
+  Context `{B : A -> Type}.
+
+  (* [hlist_combine [x_1; ... x_n] [ys_1; ... ys_n] = 
+     [x_1::ys_1; ... x_n::ys_n; x_2::ys_1 ... x_n::ys_n]] *)
+  Fixpoint hlist_combine t (lt : list A) 
+    (xl : list (B t)) (ys : list (hlist lt)) : list (hlist (t::lt)) :=
+    match xl with
+    | [] => []
+    | x::xs => map (fun y_i => x:::y_i) ys ++ hlist_combine xs ys
+    end.
+
+  Lemma hlist_combine_In a lt (x : B a) (ys : hlist lt) all_x all_ys : 
+    In x all_x -> In ys all_ys ->
+    In (x:::ys) (hlist_combine all_x all_ys).
+  Proof.
+    induction all_x; crunch.
+  Qed.
+
+  Lemma hlist_combine_hd a lt (x : hlist (a :: lt)) xs ys :
+    In x (hlist_combine xs ys) ->
+    In (hhd x) xs.
+  Proof.
+    induction xs; repeat (hlist_simpl; crunch; list_simpl).
+  Qed.
+
+  Lemma map_In_head a lt (x : hlist (a::lt)) (el : B a) xs :
+    In x (map (fun tail => el ::: tail) xs) ->
+    hhd x = el.
+  Proof.
+    repeat (list_simpl; crunch).
+  Qed.
+
+  Hint Resolve hlist_combine_hd map_In_head.
+
+  Lemma hlist_combine_NoDup (a : A) lt all_x all_ys : 
+    NoDup all_x -> NoDup all_ys ->
+    NoDup (hlist_combine (t:=a)(lt:=lt) all_x all_ys).
+  Proof.
+    induction all_x; 
+      repeat progress
+        (crunch; hlist_simpl; NoDup_simpl;
+         try
+           match goal with
+           | H : In ?x (map (fun _ => ?elt ::: _) _) |- _ =>
+               assert (hhd x = elt) by crunch
+           end
+        ).
+  Qed.
+
+  Fixpoint hlist_prod_tuple (lt : list A) (l : hlist (B := fun T => list (B T)) lt)
+    : list (hlist lt) :=
+    match l in hlist lt return list (hlist lt) with
+    | HNil => [HNil]
+    | HCons _ _ x l' => hlist_combine x (hlist_prod_tuple l')
+    end.
+
+End HList_prods.
+
+(*
+Eval vm_compute in hlist_prod_tuple ([1; 2]:::[false;true]:::HNil).
+*)
+
+Section ExhaustiveHList.
+
+  Variable A : Type.
+  Variable B : A -> Type.
+  Variable l : list A.
+
+  Context {EL : forall x, ExhaustiveList (B x)}.
+
+  Global Program Instance ExhaustiveHList : ExhaustiveList (hlist l) :=
+    { exhaustive_list := 
+        hlist_prod_tuple (hbuild _ (fun x => @exhaustive_list _ (EL x)) l)
+    }.
+  Next Obligation.
+    induction x; crunch; apply hlist_combine_In; crunch.
+  Qed.
+
+  Variable NoDup_EL : forall x, NoDup (EL x).
+
+  Hint Constructors NoDup.
+  Hint Resolve @hlist_combine_NoDup.
+
+  Lemma NoDup_ExhaustiveHList : NoDup ExhaustiveHList.
+  Proof.
+    simpl; induction l; crunch.
+  Qed.
+
+End ExhaustiveHList.
diff --git a/hlist_aux.v b/hlist_aux.v
new file mode 100644
index 0000000..c4c0e18
--- /dev/null
+++ b/hlist_aux.v
@@ -0,0 +1,234 @@
+Require Export hybrid.tactics.
+Require Export hybrid.util.
+Require Import hybrid.list_util.
+Require Export Coq.Lists.List.
+Require Export Coq.Program.Program.
+Require Import CoLoR.Util.Vector.VecUtil.
+
+Set Implicit Arguments.
+
+Section list_head.
+
+  Variable A : Type.
+
+  Program Definition head (l : list A) : nil <> l -> A :=
+    match l as l return l <> [] -> A with
+    | [] => fun H => !
+    | x::xs => fun _ => x
+    end.
+
+End list_head.
+
+Section hlists_def.
+
+  Context `{B : A -> Type}.
+
+  Inductive hlist (l : list A) : Type :=
+  | HNil : forall `{l = nil}, hlist l
+  | HCons : forall `{H : nil <> l}, B (head H) -> hlist (tail l) -> hlist l.
+
+End hlists_def.
+
+Notation "'hnil'" := (HNil (H:=refl_equal _)).
+Notation "x ::: xs" := (HCons (H:=@nil_cons _ _ _) x xs) (at level 60).
+
+Section hlists_funs.
+
+(* FIXME, use context when switching to 8.3
+  Context `{B : A -> Type, l : list A, a : A}.
+*)
+  Variable (A : Type) (B : A -> Type) (l : list A) (a : A).
+
+  Program Definition hhd (hl : hlist (a::l)) : B a :=
+    match hl with
+    | HNil _ => !
+    | HCons _ x xs => x
+    end.
+
+  Program Definition htl (hl : hlist (B:=B) (a::l)) : hlist l :=
+    match hl with
+    | HNil _ => !
+    | HCons _ x xs => xs
+    end.
+
+  (** [hsingleton x] is a [HList] with only one element [x] *)
+  Definition hsingleton (t : A) (x : B t) : hlist [t] := x:::hnil.
+
+  Variable f : forall x, B x.
+
+  (** [hbuild [t_1; ... t_n] = [f t_1; ... f t_n]] *)
+  Fixpoint hbuild (lt : list A) : hlist lt :=
+    match lt with
+    | nil => hnil
+    | x::lt' => f x ::: hbuild lt'
+    end.
+
+End hlists_funs.
+
+Ltac hlist_simpl :=
+  repeat 
+    match goal with
+    | hl : hlist [] |- _ => dep_destruct hl
+    | hl : hlist (_::_) |- _ => dep_destruct hl
+    | H : _:::_ = _:::_ |- _ => inversion H; clear H
+    end.
+
+(** Decidability of Leibniz equality on [hlist]s (given deecidable 
+    equality on all types of its elements). *)
+Section hlist_eqdec.
+
+  Context `{B : A -> Type, lt : list A}.
+  Variable EltsEqDec : forall x, In x lt -> EqDec (B x) eq.
+
+  Lemma hlist_eq_fst_eq a lt (x y : B a) (xs ys : hlist lt) :
+    x:::xs === y:::ys ->
+    x === y.
+  Proof.
+    inversion 1; dep_subst; intuition.
+  Qed.
+
+  Lemma hlist_eq_snd_eq a lt (x y : B a) (xs ys : hlist lt) :
+    x:::xs === y:::ys ->
+    xs === ys.
+  Proof.
+    inversion 1; dep_subst; intuition.
+  Qed.
+
+  Global Hint Resolve hlist_eq_fst_eq hlist_eq_snd_eq.
+
+  Global Program Instance hlist_EqDec : EqDec (hlist (B:=B) lt) eq.
+  Next Obligation.
+(*
+    revert x y; induction lt; intros; hlist_simpl; crunch;
+      match goal with
+      | EQ : forall x, ?a = x \/ In x ?l -> _, x : B ?a, y : B ?a 
+          |- context [?x:::_ === ?y:::_] =>
+          let a_al0 := fresh "a_al0" in
+          assert (a_al0 : In a (a :: l)) by intuition;
+          destruct (EQ a a_al0 x y)
+      end;
+      match goal with
+      | IH : (forall x, In x ?l -> EqDec (?B x) eq) -> forall x y, {x === y} + {x =/= y} 
+          |- context [_:::?xs === _:::?ys] =>
+          let IHpre := fresh "IHpre" in
+          assert (IHpre : forall x, In x l -> EqDec (B x) eq) by intuition;
+          destruct (IH IHpre xs ys)
+      end;
+      simpl_eqs; crunch; compute; crunch.
+*)
+  Admitted.
+
+End hlist_eqdec.
+
+Section HList_prods.
+
+  Context `{B : A -> Type}.
+
+  (* [hlist_combine [x_1; ... x_n] [ys_1; ... ys_n] = 
+     [x_1::ys_1; ... x_n::ys_n; x_2::ys_1 ... x_n::ys_n]] *)
+  Fixpoint hlist_combine t (lt : list A) 
+    (xl : list (B t)) (ys : list (hlist lt)) : list (hlist (t::lt)) :=
+    match xl with
+    | [] => []
+    | x::xs => map (fun y_i => x:::y_i) ys ++ hlist_combine xs ys
+    end.
+
+  Lemma hlist_combine_In a lt (x : B a) (ys : hlist lt) all_x all_ys : 
+    In x all_x -> In ys all_ys ->
+    In (x:::ys) (hlist_combine all_x all_ys).
+  Proof.
+    induction all_x; crunch.
+  Qed.
+
+  Lemma hlist_combine_hd a lt (x : hlist (a :: lt)) xs ys :
+    In x (hlist_combine xs ys) ->
+    In (hhd x) xs.
+  Proof.
+    induction xs; repeat (hlist_simpl; crunch; list_simpl).
+  Qed.
+
+  Lemma map_In_head a lt (x : hlist (a::lt)) (el : B a) xs :
+    In x (map (fun tail => el ::: tail) xs) ->
+    hhd x = el.
+  Proof.
+    repeat (list_simpl; crunch).
+  Qed.
+
+  Hint Resolve hlist_combine_hd map_In_head.
+
+  Lemma hlist_combine_NoDup (a : A) lt all_x all_ys : 
+    NoDup all_x -> NoDup all_ys ->
+    NoDup (hlist_combine (t:=a)(lt:=lt) all_x all_ys).
+  Proof.
+    induction all_x; 
+      repeat progress
+        (crunch; hlist_simpl; NoDup_simpl;
+         try
+           match goal with
+           | H : In ?x (map (fun _ => ?elt ::: _) _) |- _ =>
+               assert (hhd x = elt) by crunch
+           end
+        ).
+  Qed.
+
+  Program Fixpoint hlist_prod_tuple (lt : list A) (l : hlist (B := fun T => list (B T)) lt) :
+    list (hlist (B:=B) lt) :=
+    match lt with
+    | [] => [hnil]
+    | t::ts => 
+        match l with
+        | HNil _ => !
+        | HCons _ x xs =>
+            let w := @hlist_prod_tuple _ xs in _
+        end
+    end.
+   (* FIXME, this is akward... get rid of the obligation *)
+  Next Obligation.
+  Proof.
+    exact (@hlist_combine t ts x (hlist_prod_tuple _ xs)).
+  Defined.
+
+End HList_prods.
+
+Section ExhaustiveHList.
+
+  Variable A : Type.
+  Variable B : A -> Type.
+  Variable l : list A.
+
+  Context {EL : forall x, ExhaustiveList (B x)}.
+
+  Global Program Instance ExhaustiveHList : ExhaustiveList (hlist l) :=
+    { exhaustive_list := 
+        hlist_prod_tuple (hbuild _ (fun x => @exhaustive_list _ (EL x)) l)
+    }.
+  Next Obligation.
+  Admitted.
+
+  Variable NoDup_EL : forall x, NoDup (EL x).
+
+  Hint Constructors NoDup.
+  Hint Resolve @hlist_combine_NoDup.
+
+  Lemma NoDup_ExhaustiveHList : NoDup ExhaustiveHList.
+  Proof.
+    simpl; induction l; crunch.
+  Qed.
+
+End ExhaustiveHList.
+
+Section hlist_map.
+
+  Variable A C : Type.
+  Variable B : A -> Type.
+  Variable n : nat.
+  Variable l : vector A n.
+  Variable f : forall i (ip : (i < n)%nat), B (Vnth l ip) -> C.
+
+  Definition hlist_map (f : forall i (ip : (i < n)%nat), B (Vnth l ip) -> C) :
+    hlist (B:=B) (list_of_vec l) -> 
+    vector C n.
+  Proof.
+  Admitted.
+
+End hlist_map.
diff --git a/hypercube_abstraction.v b/hypercube_abstraction.v
new file mode 100644
index 0000000..739f840
--- /dev/null
+++ b/hypercube_abstraction.v
@@ -0,0 +1,272 @@
+Require Import hybrid.hypergeometry.
+Require Import hybrid.util.
+Require Import hybrid.c_util.
+Require Import hybrid.hlist_aux.
+Require Import hybrid.square_abstraction.
+Require Import hybrid.vector_setoid.
+Require Import hybrid.monotonic_flow.
+Require Import hybrid.stability.
+
+Require Import CoLoR.Util.Vector.VecUtil.
+
+Set Implicit Arguments.
+
+Open Scope CR_scope.
+
+Section contents.
+
+  (* Let's fix a dimension *)
+
+  Variable n : nat.
+
+  Definition forallDim (F : forall i, (i < n)%nat -> Type) := 
+    forall i (ip : (i < n)%nat), F i ip.
+
+  (* If one has a concrete hybrid system.. *)
+
+  Variable chs : concrete.System.
+
+  (* .. and points in that system basically correspond to points in the plane.. *)
+
+  Notation proj_morpher := 
+    (morpher (@st_eq (concrete.Point chs) ==> @st_eq CRasCSetoid)%signature).
+
+  Variable proj : vector proj_morpher n.
+
+  Hypothesis xyp : HyperPoint n -> concrete.Point chs.
+  
+  Definition pxy (p : concrete.Point chs) : HyperPoint n :=
+    Vmap (fun pi : proj_morpher => pi p) proj.
+
+  Hypotheses
+    (xyp_pxy: forall p, xyp (pxy p) = p)
+      (* TODO: should we split this condition into separate dimensions, like in square_abstraction? *)
+    (pxy_xyp: forall p, pxy (xyp p) = p). 
+
+  (* .. and flow in that system is separable over the two axes.. *)
+
+  Variables
+    (flows : concrete.Location chs -> vector (Flow CRasCSetoid) n)
+    (flow_inv : concrete.Location chs -> 
+      forall i (ip : (i < n)%nat), OpenRange -> OpenRange -> OpenRange)
+    (flow_inv_correct : forall l,
+      forallDim (fun i ip => range_flow_inv_spec (Vnth (flows l) ip) (flow_inv l ip)))
+    (flow_separable : forall l p t,
+      concrete.flow chs l p t = xyp (vector_flow (flows l) (pxy p) t)).
+
+  (* .. and on both axes, abstraction parameters can be formed based on
+   OpenRange regions.. *)
+
+  Context (A : Set) (B : A -> Set).
+
+  Context
+    (intervals : vector A n)
+    (intervals_eq_dec : forall x, EquivDec.EqDec (B x) eq)
+    (intervals_enum : forall x, ExhaustiveList (B x))
+    (intervals_NoDup : forall x, NoDup (intervals_enum x))
+    (intervals_range : forallDim (fun i ip => B (Vnth intervals ip) -> OpenQRange))
+    (absInterval : forall (l : concrete.Location chs) (p : concrete.Point chs), concrete.invariant (l, p) ->
+      forallDim (fun i ip =>
+        DN { int : B (Vnth intervals ip) | in_orange (intervals_range i ip int) (Vnth (pxy p) ip)}
+    )).
+
+  Definition ap_inv_DN :
+    forall (i : nat) (ip : (i < n)%nat) (l : concrete.Location chs) (p : concrete.Point chs),
+      concrete.invariant (l, p) ->
+      DN {i : B (Vnth intervals ip) | in_orange (intervals_range ip i) (Vnth proj ip p)}.
+  Proof.
+    intros. set (w := absInterval l p H (ip:=ip)). simpl in w.
+    unfold pxy in w. rewrite Vnth_map in w. exact w.
+  Qed.
+
+  Definition ap : abstract.Space chs :=
+    abstract.hyper_space 
+      (list_of_vec (Vbuild (fun i (ip : (i < n)%nat) =>
+         interval_abstraction.space chs (Vnth proj ip) (intervals_NoDup _) (intervals_range _) (@ap_inv_DN i ip)
+      ))).
+
+  Definition region2range :
+    forall (i : nat) (ip : (i < n)%nat),
+      abstract.Region
+        (Vnth (Vbuild (fun i (ip : (i < n)%nat) =>
+          interval_abstraction.space chs (Vnth proj ip) (intervals_NoDup _) (intervals_range _) (@ap_inv_DN i ip)
+        )) ip) -> OpenQRange.
+  Proof.
+    intros.
+    rewrite Vbuild_nth in X.
+    exact (intervals_range ip X).
+  Defined.
+
+  Definition square : abstract.Region ap -> OpenQHCube n :=
+    hlist_map _ region2range.
+
+  (*  .. then we can define useful things.
+
+  For instance, we can easily make an invariant overestimator 
+  (if one's invariant can be overestimated by a list of open squares): *)
+
+  Section invariant_overestimator.
+
+    Variable invariant_squares :
+      forall l : concrete.Location chs, 
+        { s : OpenHCube n | forall p, concrete.invariant (l, p) -> in_ohypercube (pxy p) s }.
+
+    Program Definition make_invariant_overestimator : overestimator (@abstract.invariant _ ap) := _.
+    Admit Obligations.
+(*      fun li => overestimate_osquares_overlap eps (invariant_squares (fst li)) (square (snd li)).*)
+
+  End invariant_overestimator.
+
+  (* Similarly, if one's initial condition can be overestimated by
+   an open square, we can make an initial_dec thingy. *)
+
+  Section make_initial_overestimator.
+
+    Variables
+      (initial_location : concrete.Location chs)
+      (initial_square : OpenHCube n)
+      (initial_representative : forall s, concrete.initial s ->
+        fst s = initial_location /\ in_ohypercube (pxy (snd s)) initial_square).
+
+    Program Definition make_initial_overestimator (eps : Qpos) : overestimator (@abstract.Initial _ ap) := 
+      fun s => _.
+    Admit Obligations.
+(*
+        (overestimate_conj (overestimate_osquares_overlap eps (initial_square) (square (snd s)))
+          (decision_overestimation (concrete.Location_eq_dec chs (fst s) initial_location))).
+*)
+
+  End make_initial_overestimator. 
+  
+  (* And similarly, if one's guard conditions can be overestimated by
+  open squares, we can make a guard_dec thingy. *)
+
+  Section make_guard_overestimator.
+
+    Definition GuardSquare l l' := 
+      { s : option (OpenHCube n) | forall p, concrete.guard chs (l, p) l' ->
+          match s with
+          | None => False
+          | Some v => in_ohypercube (pxy p) v
+          end
+      }.
+
+    Program Definition guard_dec (guard_square : forall l l', GuardSquare l l') (eps : Qpos) : 
+      overestimator (@abstract.guard _ ap) := 
+      _.
+    Admit Obligations.
+(*
+      fun l r l' =>
+      match guard_square l l' with
+      | Some s => overestimate_osquares_overlap eps s (square r)
+      | None => false
+      end.
+*)
+
+  End make_guard_overestimator.  
+
+  (* If the safety condition can be overestimated by a list of unsafe
+   osquares, then we can select the unsafe abstract states automatically: *)
+
+  Section square_safety.
+
+    Variables
+      (unsafe_concrete : concrete.State chs -> Prop)
+      (unsafe_squares : concrete.Location chs -> list (OpenHCube n))
+      (unsafe_squares_correct: forall s, unsafe_concrete s -> exists q,
+        In q (unsafe_squares (fst s)) /\ in_ohypercube (pxy (snd s)) q)
+      (eps: Qpos).
+
+      Program Definition unsafe_abstract : abstract.CompleteCoverList ap unsafe_concrete :=
+        _.
+(*
+      := flat_map (fun l => map (pair l) (flat_map (fun q =>
+        filter (fun s => overestimate_osquares_overlap eps q (square s)) exhaustive_list
+        ) (unsafe_squares l))) (concrete.locations chs).
+*)
+      Admit Obligations.
+
+  End square_safety.
+
+  (* Everything above is pretty simplistic. We now prepare for more complex
+   transition overestimators, for which we will require some more stuff: *)
+
+  Let reset_function := concrete.Location chs -> concrete.Location chs -> Reset.
+
+  Variables
+    (invariant_overestimator : overestimator (@abstract.invariant _ ap))
+    (guard_decider : overestimator (@abstract.guard _ ap))
+    (reset : vector reset_function n)
+    (reset_components : forall p l l', 
+      pxy (concrete.reset chs l l' p) = 
+      Vmap2 (fun resetF => apply_Reset (resetF l l')) reset (pxy p)).
+
+(*
+  Section disc_trans_regions.
+
+    Variables (eps: Qpos) (l l': concrete.Location chs) (r: abstract.Region ap).
+
+    Definition map_orange' (f: sigT increasing): OpenRange -> OpenRange
+      := let (_, y) := f in map_orange y.
+
+    Definition x_regions :=
+      match reset_x l l' with
+      | Reset_const c => filter (fun r' => overestimate_oranges_overlap eps
+        (* (map_orange' (increasing_const' c) (Xinterval_range (fst r))) (Xinterval_range r')) Xintervals *)
+        (unit_range c: OpenRange) (Xinterval_range r')) Xintervals
+      | Reset_map f => filter (fun r' => overestimate_oranges_overlap eps
+        (map_orange' f (Xinterval_range (fst r))) (Xinterval_range r')) Xintervals
+      | Reset_id => [fst r] (* x reset is id, so we can only remain in this x range *)
+      end.
+
+    Definition y_regions :=
+      match reset_y l l' with
+      | Reset_const c => filter (fun r' => overestimate_oranges_overlap eps
+        (unit_range c: OpenRange) (Yinterval_range r')) Yintervals
+      | Reset_map f => filter (fun r' => overestimate_oranges_overlap eps
+        (map_orange' f (Yinterval_range (snd r))) (Yinterval_range r')) Yintervals
+      | Reset_id => [snd r] (* x reset is id, so we can only remain in this x range *)
+      end.
+
+    Definition disc_trans_regions: list (abstract.Region ap)
+      :=
+      if overestimation_bool (guard_decider l r l') &&
+          overestimation_bool (invariant_overestimator (l, r)) then
+       filter (fun s => overestimation_bool (invariant_overestimator (l', s))) (cart x_regions y_regions)
+     else [].
+
+  End disc_trans_regions.
+
+  Definition raw_disc_trans (eps: Qpos) (s: abstract.State ap): list (abstract.State ap) :=
+    let (l, r) := s in
+    flat_map (fun l' => map (pair l') (disc_trans_regions eps l l' r)) (concrete.locations chs).
+
+  Lemma NoDup_disc_trans eps s: NoDup (raw_disc_trans eps s).
+
+  Hint Resolve in_map_orange.
+
+  Definition is_id_reset (r: Reset): bool :=
+    match r with
+    | Reset_id => true
+    | _ => false
+    end.
+
+  Hint Unfold abstract.invariant abstract.guard.
+
+  Lemma respects_disc (eps: Qpos) (s1 s2 : concrete.State chs):
+    concrete.disc_trans s1 s2 -> forall i1, abstract.in_region ap (snd s1) i1 ->
+    DN (exists i2, abstract.in_region ap (snd s2) i2 /\
+    In (fst s2, i2) (raw_disc_trans eps (fst s1, i1))).
+
+  Program Definition disc_trans: Qpos ->
+    abstract.sharing_transition_overestimator ap (@concrete.disc_trans chs) := raw_disc_trans.
+
+  Program Definition cont_trans_cond_dec eps l r r':
+    overestimation (abstract.cont_trans ap l r r') :=
+      square_flow_conditions.decide_practical
+        (xflow_invr l) (yflow_invr l) (square r) (square r') eps &&
+      invariant_overestimator (l, r) &&
+      invariant_overestimator (l, r').
+*)
+
+End contents.
diff --git a/hypergeometry.v b/hypergeometry.v
new file mode 100644
index 0000000..f96faa9
--- /dev/null
+++ b/hypergeometry.v
@@ -0,0 +1,16 @@
+
+Require Import Morphisms.
+Require Export hybrid.geometry.
+Require Export hybrid.vector_setoid.
+
+Set Implicit Arguments.
+Open Local Scope CR_scope.
+
+Definition HCube n : Type := vector Range n.
+Definition OpenQHCube n : Set := vector OpenQRange n.
+Definition OpenHCube n : Type := vector OpenRange n.
+
+Definition HyperPoint n : CSetoid := vecCSetoid CRasCSetoid n.
+
+Definition in_ohypercube n (p : HyperPoint n) (s : OpenHCube n) : Prop :=
+  Vforall2n in_orange s p.
diff --git a/list_util.v b/list_util.v
index 1178c2c..0dd04e0 100644
--- a/list_util.v
+++ b/list_util.v
@@ -337,7 +337,7 @@ Section ExhaustivePairList.
 
   Context {A B} {EA: ExhaustiveList A} {EB: ExhaustiveList B}.
 
-  Instance ExhaustivePairList:
+  Global Instance ExhaustivePairList:
      ExhaustiveList (A*B)
       := { exhaustive_list := flat_map (fun i => map (pair i) EB) EA }.
   Proof.
@@ -360,8 +360,6 @@ Section ExhaustivePairList.
   Qed.
 
 End ExhaustivePairList.
-Existing Instance ExhaustivePairList.
-  (* No idea why this is necessary... *)
 
 Instance decide_exists_in `{forall x: T, decision (P x)} l: decision (exists x, In x l /\ P x).
 Proof.
@@ -431,3 +429,47 @@ Section carts.
   Qed.
 
 End carts.
+
+Section List_prods.
+
+  Variable A : Type.
+
+  (* [list_combine [x_1; ... x_n] [y_1; ... y_n] = [x_1::y_1; ... x_n::y_n; x_2::y_1 ... x_n::y_n]] *)
+  Fixpoint list_combine (l : list A) (l' : list (list A)) : list (list A) :=
+    match l with
+    | [] => []
+    | x::xs => List.map (fun y_i => x::y_i) l' ++ list_combine xs l'
+    end.
+
+  (* list_prod_tuple [xs_1; ... xs_n] gives a list containing every 
+     list of the form [x_1; ... x_n] where [In x_1 xs_1], ... [In x_n xs_n].
+   *)
+  Fixpoint list_prod_tuple (elts : list (list A)) : list (list A) :=
+    match elts with
+    | [] => [[]]
+    | x::xs => list_combine x (list_prod_tuple xs)
+    end.
+
+End List_prods.
+
+(*
+Eval vm_compute in list_combine [1; 2] [[3;4]; [5;6]].
+Eval vm_compute in list_prod_tuple [[1;2]; [3;4]; [5;6]].
+*)
+
+Ltac NoDup_simpl :=
+  repeat
+    match goal with
+    | |- NoDup (_ ++ _) => apply NoDup_app
+    | |- NoDup (map _ _) => apply NoDup_map
+    | H : NoDup (_::_) |- _ => inversion H; clear H
+    end.
+
+Ltac list_simpl :=
+  repeat 
+    match goal with
+    | H : In _ (?l ++ ?m) |- _ => 
+        destruct (in_app_or l m _ H); clear H
+    | H : In _ (map _ _) |- _ => 
+        destruct (proj1 (in_map_iff _ _ _) H); clear H
+    end.
diff --git a/nat_util.v b/nat_util.v
index 061f294..ca924f8 100644
--- a/nat_util.v
+++ b/nat_util.v
@@ -2,6 +2,8 @@ Require Export Arith.
 Require Export Peano_dec.
 Require Import util.
 Require Import EqdepFacts.
+Require Import stability.
+Require Import tactics.
 
 Set Implicit Arguments.
 
@@ -61,46 +63,93 @@ Section Check_n.
 
   Variables 
     (n : nat) 
-    (P : forall i, i < n -> Prop).
-
-  Program Fixpoint check_n_aux (p : nat | p <= n) 
-    {measure (fun p => n - p) p} : Prop :=
+    (P Q : forall i, i < n -> Prop).
 
-    match le_lt_dec n p with
-    | left _ => True
-    | right cmp =>
-        @P p cmp /\ @check_n_aux (S p)
+  Obligation Tactic := crunch.
+
+  Program Fixpoint check_n_aux (p : nat) (H : p < n) : Prop :=
+    let this := @P p H in
+    let rest := 
+      match p with
+      | 0 => True
+      | S p' => @check_n_aux p' _
+      end
+    in
+    this /\ rest.
+
+  Program Definition check_n := 
+    match n with
+    | 0 => True
+    | _ => @check_n_aux (pred n) _
     end.
 
-  Next Obligation.
+  Variable P_holds : forall i (ip: i < n), P ip.
+
+  Lemma check_n_holds_aux : 
+    forall i (ip : i < n), check_n_aux ip.
   Proof.
-    omega.
+    induction i; crunch.
   Qed.
 
-  Program Definition check_n := @check_n_aux 0.
+  Variable P_stable : forall i (ip: i < n), Stable (P ip).
 
-  Next Obligation.
+  Lemma check_n_Stable_aux :
+    forall i (ip : i < n), Stable (check_n_aux ip).
   Proof.
-    omega.
+    induction i; crunch.
   Qed.
 
-  Lemma check_n_holds : 
-    (forall i (ip: i < n), P ip) -> check_n.
-  Proof.
-  Admitted.
-
 End Check_n.
 
+Lemma check_n_holds n (P : forall i, i < n -> Prop) : 
+  (forall i (ip: i < n), P i ip) -> check_n P.
+Proof.
+  destruct n; crunch.
+  apply check_n_holds_aux; crunch.
+Qed.
+
+Lemma check_n_Stable n (P : forall i, i < n -> Prop) : 
+  (forall i (ip: i < n), Stable (P i ip)) -> Stable (check_n P).
+Proof.
+  destruct n; crunch.
+  apply check_n_Stable_aux; crunch.
+Qed.
+
 Section Check_n_equiv.
 
   Variables 
     (n : nat)
-    (P Q : forall i, i < n -> Prop).
+    (P Q : forall i, i < n -> Prop)
+    (P_eq_Q : forall i (ip : i < n), P ip <-> Q ip).
 
-  Lemma check_n_equiv : 
-    (forall i (ip : i < n), P ip <-> Q ip) ->
-    (check_n P <-> check_n Q).
+  Lemma check_n_equiv_aux : 
+    forall i (ip : i < n), 
+      check_n_aux P ip <-> check_n_aux Q ip.
   Proof.
-  Admitted.
+     (* FIXME, there must be a better way to state this proof, without 
+        those asserts (which essentially break iff into two implications *)
+    pose (fun i (ip : i < n) => proj1 (P_eq_Q ip)).
+    pose (fun i (ip : i < n) => proj2 (P_eq_Q ip)).
+    induction i.
+    crunch.
+    pose (fun ip : i < n => proj1 (IHi ip)).
+    pose (fun ip : i < n => proj2 (IHi ip)).
+    crunch.
+  Qed.
+
+End Check_n_equiv.
 
-End Check_n_equiv.
\ No newline at end of file
+Lemma check_n_equiv n 
+  (P Q : forall i, i < n -> Prop)
+  (P_eq_Q : forall i (ip : i < n), P i ip <-> Q i ip) :
+  check_n P <-> check_n Q.
+Proof.
+  destruct n; intros.
+  crunch.
+  unfold check_n.
+  match goal with
+    | |- check_n_aux _ ?ip <-> check_n_aux _ ?jp =>
+      rewrite (lt_unique ip jp)
+  end.
+  apply check_n_equiv_aux. trivial.
+Qed.
diff --git a/square_flow_conditions.v b/square_flow_conditions.v
index 7ed2d00..7fe4b32 100644
--- a/square_flow_conditions.v
+++ b/square_flow_conditions.v
@@ -107,6 +107,8 @@ Section contents.
 End contents.
 End one_axis.
 
+Hint Resolve one_axis.flow_range_covers.
+
 Section contents.
 
   Variables
@@ -181,3 +183,4 @@ Section contents.
   Qed.
 
 End contents.
+
diff --git a/stability.v b/stability.v
index 8203588..d72e669 100644
--- a/stability.v
+++ b/stability.v
@@ -8,11 +8,15 @@ Hint Unfold DN.
 Definition DN_return {T: Type}: T -> DN T :=
   fun x f => f x.
 
+Notation "'return' x" := (DN_return x) (at level 30).
+
 Hint Resolve @DN_return.
 
 Definition DN_bind {A: Type}: DN A -> forall B, (A -> DN B) -> DN B :=
   fun X Y Z P => X (fun a => Z a P).
 
+Notation "x <- e ; t" := (DN_bind e _ (fun x => t)) (right associativity, at level 60).
+
 Definition ext_eq: Prop := forall (A B: Type) (f g: A -> B), (forall x, f x = g x) -> f = g.
 
 Lemma DN_runit: ext_eq -> forall A (x: DN A),
diff --git a/tactics.v b/tactics.v
new file mode 100644
index 0000000..2d098ee
--- /dev/null
+++ b/tactics.v
@@ -0,0 +1,155 @@
+Require Export Coq.omega.Omega.
+Require Import Coq.Bool.Bool.
+Require Export Coq.Classes.EquivDec.
+Require Export Coq.Program.Program.
+Require Export Coq.Setoids.Setoid.
+
+(** * A bunch of useful tactics (and abbreviations). *)
+
+(** Varia *)
+
+Ltac ref := reflexivity.
+
+Ltac hyp := assumption.
+
+Ltac sym := symmetry.
+
+Ltac arith_contr := elimtype False; omega.
+
+Ltac ded h := generalize h; intro.
+
+Ltac ssimpl := simpl in *; try subst. 
+
+Ltac easy := ssimpl; auto.
+
+(** Cleaning the proof context *)
+
+Ltac remove_dup_hyps := repeat
+  match goal with
+  | H: ?X, H': ?X |- _ => clear H'
+  end.
+
+Ltac clear_all := repeat
+  match goal with
+  | H: _ |- _ => clear H
+  end.
+
+Ltac remove_trivial_equalities := repeat
+  match goal with
+  | H: ?X = ?X |- _ => clear H
+  end.
+
+Ltac clean := remove_trivial_equalities; remove_dup_hyps.
+
+(** Equality simplification *)
+
+Require Import Coq.Classes.Equivalence.
+
+Ltac simpl_eq :=
+  match goal with
+  | H: ?X = ?X |- _ => clear H
+  | H: _ = _ |- _ => progress (simplify_eq H; intros; try subst; remove_dup_hyps)
+  | H: _ === _ |- _ => rewrite H; clear H
+  end.
+
+Ltac simpl_eqs := repeat simpl_eq.
+
+(** Hypothesis decomposition *)
+
+Ltac decomp_hyp H := 
+  match type of H with
+  | _ /\ _ => decompose [and] H; clear H
+  | _ \/ _ => decompose [or] H; clear H
+  | ex _ => decompose [ex] H; clear H
+  | sig _ => decompose record H; clear H
+  end.
+
+Ltac decomp :=
+  repeat
+    match goal with
+    | H: _ |- _ => decomp_hyp H
+    end.
+
+(** Dependent rewriting *)
+
+Ltac dep_rewrite :=
+  match goal with
+  | H : existT ?A ?a ?b = existT ?A ?a ?c |- _ => 
+      let eq := fresh "eq" in
+        set (eq := inj_pairT2 _ A _ _ _ H); clearbody eq; rewrite eq in *; clean
+  | H : ?x = _ |- _ => subst x
+  | H : _ = ?x |- _ => subst x
+  end.
+
+Ltac dep_subst := repeat progress (clean; try dep_rewrite; try subst).
+
+(** Inversion *)
+
+Ltac invert H := inversion H; try subst.
+
+Ltac dep_invert H := inversion H; dep_subst.
+
+(** Boolean simplifications *)
+
+Ltac bool_case :=
+  repeat progress (bool_simpl ||
+    match goal with
+    | H: ?X || ?Y = true |- _ => destruct (orb_true_elim _ _ H); clear H
+    end)
+
+with bool_solve := 
+  repeat split; intros; bool_simpl; decomp; try solve [hyp | bool_case; auto]
+
+with bool_simpl :=
+  repeat
+    match goal with
+    | H: ?X && ?Y = true |- _ => destruct (proj1 (andb_true_iff X Y) H); clear H
+    | |- ?X && ?Y = true => apply andb_true_intro; split
+    | |- ?X || ?Y = true => apply orb_true_intro
+    | |- context [?X && ?Y = true] => 
+           setoid_replace (X && Y = true) with (X = true /\ Y = true) by bool_solve
+    | |- context [?X || ?Y = true] => 
+           setoid_replace (X || Y = true) with (X = true \/ Y = true) by bool_solve
+    end.
+
+(* FIXME, this should go somewhere else but where? *)
+Notation "()" := tt.
+
+Ltac crunch :=
+  let intuition_ext := 
+    simpl in *; 
+    intuition eauto with datatypes; 
+    try subst;
+    decomp; 
+    dep_subst; 
+    try congruence
+  in
+  let solve_arith := 
+    try omega; 
+    try (elimtype False; omega) 
+  in
+  let rewriter :=
+    repeat 
+      match goal with
+      | [ H : _ |- _ ] =>
+          solve 
+            [ rewrite H; clear H; crunch
+            | rewrite <- H; clear H; crunch
+            ]
+      end
+  in
+  repeat progress (
+    intuition_ext; 
+    rewriter; 
+    intuition_ext; 
+    solve_arith
+  ).
+
+Tactic Notation "crunch" "with" tactic3(t) := repeat progress (crunch; t).
+
+Ltac dep_destruct E :=
+  let x := fresh "x" in
+    remember E as x; simpl in x; dependent destruction x;
+      try match goal with
+            | [ H : _ = E |- _ ] => rewrite <- H in *; clear H
+          end.
diff --git a/util.v b/util.v
index 84af04e..fcd6cb1 100644
--- a/util.v
+++ b/util.v
@@ -413,3 +413,5 @@ Section alternate.
 End alternate.
 
 Hint Constructors end_with.
+
+Notation "[= e =]" := (exist _ e _).
diff --git a/vector_setoid.v b/vector_setoid.v
index fed0c93..d6826c8 100644
--- a/vector_setoid.v
+++ b/vector_setoid.v
@@ -3,9 +3,12 @@ Require Export VecEq.
 Require Export CSetoids.
 Require Export SetoidClass.
 Require Import c_util.
+Require Export Coq.Classes.EquivDec.
 
 Set Implicit Arguments.
 
+(** * CSetoid on vectors. *)
+
 Section VectorCSetoid.
 
   Variables A : CSetoid.
@@ -46,8 +49,9 @@ admit.
 
 End VectorCSetoid.
 
-(* FIXME, this should come from CoLoR.Utils.Vector.VecEq.v *)
-Add Parametric Morphism A n i (ip : (i < n)%nat) : (fun v : vecCSetoid A n => Vnth v ip)
+(* FIXME, this should come from CoLoR.Util.Vector.VecEq.v *)
+Add Parametric Morphism A n i (ip : (i < n)%nat) : 
+  (fun v : vecCSetoid A n => Vnth v ip)
   with signature (@cs_eq _) ==> (@cs_eq _)
     as Vnth_Cmorph.
 
@@ -55,20 +59,17 @@ Proof.
   intros. apply Vforall2n_nth with (R := @st_eq _). assumption.
 Qed.
 
-(*
-Why setoid rewrite doesn't work with this morphism?
+(** * Decidable Leibniz equality on vectors *)
 
-Require Import Morphisms.
-Print Instances Morphism.
+Section vector_eqdec.
 
-(* Let's test it... *)
-Lemma test n (x y : vecCSetoid CRasCSetoid n) :
-  x [=] y -> forall i (ip : (i < n)%nat), Vnth x ip [=] Vnth y ip.
-Proof.
-  intros.
-  (* It's just an instance of the morphism: *)
-(*  apply Vnth_Cmorph. assumption.*)
-  (* and yet we cannot rewrite... *)
-  rewrite H.
-Qed.
-*)
+  Variable n : nat.
+  Variable A : Type.
+  Variable eqA_dec : EqDec A eq.
+
+  Global Program Instance vector_EqDec : EqDec (vector A n) eq.
+  Next Obligation.
+    apply eq_vec_dec; auto.
+  Qed.
+
+End vector_eqdec.