diff --git a/ArrayMachine.v b/ArrayMachine.v
index 9832faf..56af592 100644
--- a/ArrayMachine.v
+++ b/ArrayMachine.v
@@ -1,7 +1,8 @@
-Require Import Rushby.
-From stdpp Require Import list relations collections fin_collections.
+(** Instantiation of the intransitive interference with an "array machine" *)
+Require Import NI.Rushby.
+From stdpp Require Import list relations gmap sets fin_sets.
 
-Module ArrayMachine <: Mealy.
+Module ArrayMachine.
 
 Definition state := nat -> nat.
 Inductive command :=
@@ -23,39 +24,51 @@ Definition preform (s : state) (a : action) : state * out :=
 Definition step s a := fst (preform s a).
 Definition output s a := snd (preform s a).
 Definition initial (x : nat) := 0.
-End ArrayMachine.
 
-  
+End ArrayMachine.
 Import ArrayMachine.
-Module M := Rushby.Rushby ArrayMachine.
-Import M.
+Instance ArrayMealyMachine : Mealy state action out :=
+  { initial := initial;
+    step := step;
+    output := output }.
 
 Eval compute in (do_actions [Write 1 1] 2).
+(** ===> 0 *)
 
 Definition domain := action.
 Definition nameA := nat.
 Definition valA := nat.
-Definition observeA (u : domain) : FinSet nameA :=
+Definition observeA (u : domain) : gset nameA :=
   match u with
     | Read i => {[ i ]}
     | Write _ _ => ∅
   end.
-Definition alterA (u : domain) : FinSet valA :=
+Definition alterA (u : domain) : gset valA :=
   match u with
     | Read _ => ∅
     | Write i _ => {[ i ]}
   end.
 
 
-Instance domain_dec : forall (u v : domain), Decision (u = v).
-Proof. intros.
+Instance domain_dec : EqDecision domain.
+Proof. intros u v.
 unfold Decision.
 repeat (decide equality).
 Defined.
 
-Instance arraymachine_ss : StructuredState domain := 
+Instance domain_countable : Countable domain.
+ refine (inj_countable' (λ x, match x with
+  | Write i1 i2 => (inl (i1, i2))
+  | Read i => (inr i)
+  end) (λ x, match x with
+  | inl (i1, i2) => Write i1 i2
+  | inr i => Read i
+  end) _); by intros [].
+Defined.
+
+Instance arraymachine_ss : StructuredState domain :=
   { name := nameA; value := valA; contents s n := s n
-  ; observe := observeA; alter := alterA }. 
+  ; observe := observeA; alter := alterA }.
 
 Definition interference (u v : domain) :=
   (exists (n : nameA), n ∈ alterA u ∧ n ∈ observeA v).
@@ -64,59 +77,64 @@ Inductive interferenceR : relation domain :=
   | interference_refl : forall (u : domain), interferenceR u u
   | interference_step : forall (u v: domain), interference u v -> interferenceR u v.
 
-Instance policy_ss : Policy domain := 
+Instance: Set_ nameA (gset nameA).
+apply _.
+Qed.
+
+Instance policy_ss : Policy domain :=
   { policy := interferenceR
   ; dom := fun (a : action) => (a : domain) }.
 Proof.
-intros. unfold Decision. 
-destruct v as [i j | i]; destruct w as [m n | m].
-- destruct (decide (i = m)). destruct (decide (j = n)); subst; auto.
-left. constructor. 
-right. intro I. inversion I; subst. apply n0. auto. 
-inversion H. unfold observeA in *. destruct H0 as [HH HHH].
-apply (not_elem_of_empty x); assumption.
-right. intro. inversion H; subst. apply n0. auto. 
-inversion H0. unfold alterA, observeA in *. destruct H1.
-apply (not_elem_of_empty x); assumption.
-- destruct (decide (i = m)); subst. left. right. unfold interference.
-  simpl. exists m. split; apply elem_of_singleton; auto.
-  right. intro. inversion H; subst. inversion H0. simpl in H1.
-  destruct H1. apply elem_of_singleton in H1; apply elem_of_singleton in H2. subst. apply n;auto.
-- right. intro. inversion H;subst. inversion H0; subst.
-  simpl in H1; inversion H1. apply (not_elem_of_empty x); assumption.
-- destruct (decide (i = m)); subst.
-  left. constructor.
-  right. intro. inversion H; subst. auto.
-  inversion H0; subst. simpl in H1; inversion H1. eapply not_elem_of_empty. eassumption.
+- intros v w.
+  destruct v as [i j | i]; destruct w as [m n | m].
+  + destruct (decide (i = m)). destruct (decide (j = n)); subst; auto.
+    left. constructor.
+    right. intro I. inversion I; subst. apply n0. auto.
+    inversion H. unfold observeA in *. destruct H0 as [HH HHH].
+    apply (not_elem_of_empty x HHH).
+    right. intro. inversion H; subst. apply n0. auto.
+    inversion H0. unfold alterA, observeA in *. destruct H1 as [HH HHH].
+    apply (not_elem_of_empty x HHH).
+  + destruct (decide (i = m)); subst. left. right. unfold interference.
+    simpl. exists m. split; apply elem_of_singleton; auto.
+    right. intro. inversion H; subst. inversion H0. simpl in H1.
+    destruct H1. apply elem_of_singleton in H1; apply elem_of_singleton in H2. subst. apply n;auto.
+  + right. intro. inversion H;subst. inversion H0; subst.
+  simpl in H1; inversion H1. eapply (not_elem_of_empty x); eassumption.
+  + destruct (decide (i = m)); subst.
+    left. constructor.
+    right. intro. inversion H; subst. auto.
+    inversion H0; subst. simpl in H1; inversion H1.
+    eapply (not_elem_of_empty x); eassumption.
 - intro u. constructor.
 Defined.
 
-Check RefMonAssumptions.
-
 Instance rma_yay :  RefMonAssumptions.
-Proof. split; simpl; unfold RMA_partition; intros;
-       unfold contents in *; simpl in H8.
-unfold output. 
- unfold preform. destruct a as [i j | i]; simpl in *. reflexivity. 
- apply H8. apply elem_of_singleton. reflexivity.
-       
-unfold step, preform. destruct a as [i j | i]. simpl in *.
-destruct (decide (i = n)); subst; unfold extendS; simpl. 
-replace (beq_nat n n) with true; auto. apply beq_nat_refl.
-destruct H9. 
-unfold step in H9; simpl in H9. unfold extendS in H9; simpl in H9.
-replace (beq_nat n i) with false in *; auto.
-congruence. SearchAbout beq_nat false. symmetry. apply beq_nat_false_iff. omega.
-unfold step in H9; simpl in H9. unfold extendS in H9; simpl in H9.
-replace (beq_nat n i) with false in *; auto.
-congruence. symmetry. apply beq_nat_false_iff. omega.
+Proof.
+  split; simpl; unfold RMA_partition.
+  - intros a s t Hst;
+      unfold contents in *; simpl in *.
+    unfold output.
+    unfold preform. destruct a as [i j | i]; simpl in *. reflexivity.
+    apply Hst. eapply elem_of_singleton. reflexivity.
+  - intros a s t n Hst Hn.
+    unfold step, preform. destruct a as [i j | i]. simpl in *.
+    destruct (decide (i = n)); subst; unfold extendS; simpl.
+    replace (beq_nat n n) with true; auto. apply beq_nat_refl.
+    destruct Hn as [Hn|Hn].
+    unfold step in Hn; simpl in Hn. unfold extendS in Hn; simpl in Hn.
+    replace (beq_nat n i) with false in *; auto.
+    congruence. symmetry. apply beq_nat_false_iff. omega.
+    unfold step in Hn; simpl in Hn. unfold extendS in Hn; simpl in Hn.
+    replace (beq_nat n i) with false in *; auto.
+    congruence. symmetry. apply beq_nat_false_iff. omega.
 
-simpl. destruct H9; unfold step, preform in H9; simpl in H9;
+    simpl. destruct Hn as [Hn|Hn]; unfold step, preform in Hn; simpl in Hn;
        congruence.
-
-unfold step, preform in H8; simpl in H8. destruct a; simpl in *.
-unfold extendS in H8. destruct (decide (n = n0)); subst.
-apply elem_of_singleton; auto. replace (beq_nat n n0) with false in *; try (congruence). symmetry. apply beq_nat_false_iff. assumption.
+  - intros a s n Hst.
+    unfold step, preform in Hst; simpl in Hst. destruct a; simpl in *.
+    unfold extendS in Hst. destruct (decide (n = n0)); subst.
+    apply elem_of_singleton; auto. replace (beq_nat n n0) with false in *; try (congruence). symmetry. apply beq_nat_false_iff. assumption.
 congruence.
 Defined.
 
@@ -125,4 +143,3 @@ Proof.
   apply rma_secure_intransitive.
   intros u v n A1 A2. simpl.  right. firstorder.
 Qed.
-
diff --git a/Rushby.v b/Rushby.v
index 547db17..7a77690 100644
--- a/Rushby.v
+++ b/Rushby.v
@@ -1,24 +1,11 @@
-(** Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby 
+(** Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby
     www.csl.sri.com/papers/csl-92-2/
 *)
 
 (** printing -> #→# *)
 (** printing (policy a b) #a ⇝ b# *)
 
-From stdpp Require Import list relations collections fin_collections.
-Parameter FinSet : Type -> Type.
-(** begin hide **)
-Context `{forall A, ElemOf A (FinSet A)}.
-Context `{forall A, Empty (FinSet A)}.
-Context `{forall A, Singleton A (FinSet A)}.
-Context `{forall A, Union (FinSet A)}.
-Context `{forall A, Intersection (FinSet A)}.
-Context `{forall A, Difference (FinSet A)}.
-Context `{forall A, Elements A (FinSet A)}.
-Context `{forall A, Collection A (FinSet A)}.
-(* TODO: i wrote this line down so that there is a Collection -> SimpleCollection -> JoinSemiLattice instance for FinSet; how come this is not automatically picked up by the next assumption? *)
-Context `{forall A (H : EqDecision A), FinCollection A (FinSet A)}.
-(** end hide **)
+From stdpp Require Import list relations gmap sets fin_sets.
 
 (** * Mealy machines *)
 
@@ -46,10 +33,10 @@ Fixpoint run `{Mealy state action out} (s : state) (ls : list action) : state :=
 Definition do_actions `{Mealy state action out} : list action -> state := run initial.
 
 (** The [test] function runs the required list of actions and examines the output of the resulting state on a specified action. *)
-Definition test `{Mealy state action out} (ls : list action) : action -> out := output (do_actions ls).  
+Definition test `{Mealy state action out} (ls : list action) : action -> out := output (do_actions ls).
 
 Section Rushby.
-  
+
 (** We assume for the rest of the formalisation that we have a Mealy
 machine [M]. Thus, we parameterize our main development module by a machine [M].  *)
 
@@ -73,6 +60,7 @@ Class Policy (domain : Type) := {
   instances. *)
 
   domain_dec :> EqDecision domain;
+  domain_countable :> Countable domain;
   policy :> relation domain;
   policy_dec :> RelDecision policy;
   policy_refl :> Reflexive policy
@@ -83,7 +71,7 @@ Delimit Scope policy_scope with P.
 Open Scope policy_scope.
 Infix "⇝" := policy (at level 70) : policy_scope.
 
-(** Quoting Rushby: 
+(** Quoting Rushby:
 
 <<
      We wish to define security in terms of information flow, so the
@@ -136,10 +124,10 @@ Section view_partitions.
 
 (** Formally, a view partition is an assignment of an equivalence
 relation [≈{u}] for every domain [u] *)
-  
+
 Class ViewPartition (domain : Type) := {
   view_partition :> domain -> relation state;
-  view_partition_is_equiv :> forall v, Equivalence (view_partition v)
+  view_partition_is_equiv :> forall v, Equivalence (view_partition v);
 }.
 
 Notation "S ≈{ U } T" := (view_partition U S T)
@@ -149,7 +137,7 @@ Open Scope policy_scope.
 states [s, t] that are indistinguishable w.r.t. the domain [dom a],
 the output of the system [output s a] is the same as [output t a] *)
 
-Class OutputConsistent `{P : Policy domain} `(ViewPartition domain) := 
+Class OutputConsistent `{P : Policy domain} `(ViewPartition domain) :=
   output_consistent : (forall a s t, s ≈{dom a} t -> output s a = output t a).
 
 (** Our first lemma states that if we have a view partitioned system
@@ -195,15 +183,15 @@ Theorem unwinding `{P: Policy domain} `{VP: ViewPartition domain} `{@OutputConsi
 Proof.
   intros LRP SC. apply output_consist_security.
   assert (forall ls u s t, view_partition u s t -> view_partition u (run s ls) (run t (purge ls u))) as General. (* TODO: a simple generalize would not suffice, because we actually need the s ≈ t assumption *)
-    induction ls; simpl; auto.    
+    induction ls; simpl; auto.
     intros u s t HI.
     destruct (decide (policy (dom a) u)).
     (* DOESNT WORK (Lexer) : destruct (decide ((dom a) ⇝ u)). *)
-    (** Case [(dom a) ~> u] *) 
+    (** Case [(dom a) ~> u] *)
       apply IHls. apply SC; assumption.
-    (** Case [(dom a) ~/> u] *)      
-      apply IHls. 
-      transitivity s. symmetry. unfold locally_respects_policy in LRP. apply LRP; assumption. assumption.  
+    (** Case [(dom a) ~/> u] *)
+      apply IHls.
+      transitivity s. symmetry. unfold locally_respects_policy in LRP. apply LRP; assumption. assumption.
   unfold do_actions. intros ls u. apply General. reflexivity.
 Qed.
 
@@ -213,7 +201,7 @@ End view_partitions.
 
 Section ACI.
 
-(** In this section we consider a formalisation of the access control mechansisms. 
+(** In this section we consider a formalisation of the access control mechansisms.
 
 We say that the machine has _structured state_ if we have a collection
 of [name]s and [value]s (the latter being decidable), and some sort of
@@ -227,8 +215,10 @@ Class StructuredState (domain : Type)  := {
   value : Type;
   contents : state -> name -> value;
   value_dec :> EqDecision value;
-  observe : domain -> FinSet name;
-  alter : domain -> FinSet name
+  name_dec :> EqDecision name;
+  name_countable :> Countable name;
+  observe : domain -> gset name;
+  alter : domain -> gset name
 }.
 
 (** This induces the view partition relation as follows: two state [s]
@@ -240,13 +230,15 @@ Definition RMA_partition `{@StructuredState domain} (u : domain) s t := (forall
 
 Transparent RMA_partition.
 
-Instance RMA `{@StructuredState domain} : ViewPartition domain := { view_partition := RMA_partition }.
+Instance RMA `{!StructuredState domain}
+         `{!EqDecision domain, !Countable domain}
+  : ViewPartition domain := { view_partition := RMA_partition }.
 (* begin hide *)
-  intro u. split; unfold RMA_partition.
-  (* Reflexivity *) unfold Reflexive. auto.
-  (* Symmetry *) unfold Symmetric. intros x y Sy.
+  intro u. split; try apply _; unfold RMA_partition.
+  (* Reflexivity *) - unfold Reflexive. auto.
+  (* Symmetry *) - unfold Symmetric. intros x y Sy.
   symmetry. apply Sy. assumption.
-  (* Transitivity *) unfold Transitive. intros x y z T1 T2 n.
+  - (* Transitivity *) unfold Transitive. intros x y z T1 T2 n.
   transitivity (contents y n); [apply T1 | apply T2]; assumption.
 Defined. (* We have to use 'Defined' here instead of 'Qed' so that we can unfold 'RMA' later on *)
 (* end hide *)
@@ -255,18 +247,20 @@ Hint Resolve RMA.
 
 (** ** Reference monitor assumptions *)
 (* TODO: explain those assumptions *)
-Class RefMonAssumptions `{Policy domain} `{StructuredState domain} :=
-  { rma1 : forall (a : action) s t,
-             view_partition (dom a) s t -> output s a = output t a
-  ; rma2 : forall a s t n,
-             view_partition (dom a) s t ->
-             ((contents (step s a) n) ≠ (contents s n)
-                ∨ (contents (step t a) n) ≠ (contents t n))
-             -> contents (step s a) n = contents (step t a) n
-  ; rma3 :  forall a s n,
-               contents (step s a) n ≠ contents s n -> n ∈ alter (dom a)
-}.                                               
-      
+Class RefMonAssumptions `{!Policy domain, !StructuredState domain} :=
+{ rma1 :
+    forall (a : action) s t,
+      view_partition (dom a) s t -> output s a = output t a;
+  rma2 :
+    forall a s t n,
+      view_partition (dom a) s t ->
+      ((contents (step s a) n) ≠ (contents s n)
+       ∨ (contents (step t a) n) ≠ (contents t n))
+      -> contents (step s a) n = contents (step t a) n;
+  rma3 :
+    forall a s n, contents (step s a) n ≠ contents s n -> n ∈ alter (dom a)
+}.
+
 (** If the reference monitor assumptions are satisfied, then the system is output-consistent *)
 Global Instance OC `{RefMonAssumptions}: OutputConsistent RMA.
 exact rma1. Defined.
@@ -278,15 +272,15 @@ exact rma1. Defined.
 *)
 
 (* Theorem 2 *)
-Theorem RMA_secutity `{RefMonAssumptions} : 
+Theorem RMA_secutity `{RefMonAssumptions} :
   (forall u v, (policy u v) → observe u ⊆ observe v)
   -> (forall u v n, (n ∈ alter u) → (n ∈ observe v) → (policy u v))
   -> security.
 Proof.
-  intros Cond1 Cond2. apply unwinding. 
+  intros Cond1 Cond2. apply unwinding.
   (** We apply the unwinding theorem, so we have to verify that
-     we locally respect policy and that we have step-consistency *)  
-  unfold locally_respects_policy. 
+     we locally respect policy and that we have step-consistency *)
+  unfold locally_respects_policy.
   intros a u s.
 
   (** In order to prove that the system locally respects the policy
@@ -297,7 +291,7 @@ Proof.
     intros opH. destruct opH as [n [??]].
     eapply Cond2. eapply rma3. eauto. assumption.
   intros NPolicy.
-  unfold view_partition, RMA, RMA_partition. 
+  unfold view_partition, RMA, RMA_partition.
   (* TODO: why can't decide automatically pick the instance value_dec? *)
   intros. destruct (decide (contents s n = contents (step s a) n)) as [e|Ne]. assumption. exfalso. apply NPolicy. apply CP.
   exists n; split; assumption.
@@ -317,7 +311,7 @@ Proof.
   (* We use the Second RM assmption to deal with this case *)
   apply rma2. (* for this we have to show that s ~_(dom a) t *)
   unfold view_partition, RMA, RMA_partition.
-  intros m L. apply A. 
+  intros m L. apply A.
   apply Cond1 with (u:=dom a).
   apply Cond2 with (n:=n); [eapply rma3 | ]; eassumption.
   assumption.
@@ -326,7 +320,7 @@ Proof.
   (* TODO: repetition *)
   apply rma2. (* for this we have to show that s ~_(dom a) t *)
   unfold view_partition, RMA, RMA_partition.
-  intros m L. apply A. 
+  intros m L. apply A.
   apply Cond1 with (u:=dom a).
   apply Cond2 with (n:=n); [eapply rma3| ]; eassumption.
   assumption.
@@ -339,7 +333,7 @@ End ACI.
 Section Intransitive.
 
 (** Auxiliary  definitions *)
-Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : FinSet domain :=
+Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : gset domain :=
   match ls with
     | [] => {[ d ]}
     | a::tl => let src := sources tl d in
@@ -351,7 +345,7 @@ Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : FinSet domai
 Lemma sources_mon `{Policy} : forall a ls d, sources ls d ⊆ sources (a::ls) d.
 Proof.
   intros. simpl.
-  destruct (decide _); [apply union_subseteq_l |]; auto. 
+  destruct (decide _); [apply union_subseteq_l |]; auto.
 Qed.
 
 Hint Resolve sources_mon.
@@ -360,12 +354,12 @@ Lemma sources_monotone `{Policy} : forall ls js d, sublist ls js → sources ls
 Proof.
   intros ls js d M.
   induction M. simpl. reflexivity.
-  simpl. destruct (decide (∃ v : domain, v ∈ sources l1 d ∧ policy (dom x) v)); destruct (decide (∃ v : domain, v ∈ sources l2 d ∧ policy (dom x) v)).  
+  simpl. destruct (decide (∃ v : domain, v ∈ sources l1 d ∧ policy (dom x) v)); destruct (decide (∃ v : domain, v ∈ sources l2 d ∧ policy (dom x) v)).
   - apply union_mono_r. assumption.
   - exfalso. apply n. destruct e as [v [e1 e2]]. exists v; split; try (apply (IHM v)); assumption.
   - transitivity (sources l2 d). assumption. apply union_subseteq_l.
   - assumption.
-  - transitivity (sources l2 d); auto. 
+  - transitivity (sources l2 d); auto.
 Qed.
 
 Lemma sources_in `{Policy} : forall ls d, d ∈ sources ls d.
@@ -408,9 +402,13 @@ Proof.
   apply (H ls (dom a)).
 Qed.
 
-Definition view_partition_general `{ViewPartition domain} (C : FinSet domain) s t := forall (u: domain), u ∈ C -> view_partition u s t.
+Definition view_partition_general
+  `{!ViewPartition domain, !EqDecision domain, !Countable domain}
+  (C : gset domain) s t
+  := forall (u: domain), u ∈ C -> view_partition u s t.
 
-Global Instance view_partition_general_equiv `{ViewPartition domain}: 
+Global Instance view_partition_general_equiv
+  `{ViewPartition domain, !EqDecision domain, !Countable domain}:
   forall V, Equivalence (view_partition_general V).
 Proof.
   intro V. split.
@@ -422,10 +420,10 @@ Qed.
 Definition weakly_step_consistent `{Policy domain} `{ViewPartition domain} :=
   forall s t u a, view_partition u s t -> view_partition (dom a) s t -> view_partition u (step s a) (step t a).
 
-Ltac exists_inside v := 
+Ltac exists_inside v :=
   let H := fresh "Holds" in
   let nH := fresh "notHolds" in
-  destruct (decide _) as [H | []]; 
+  destruct (decide _) as [H | []];
   [ try reflexivity | exists v; try auto].
 
 Local Hint Resolve sources_mon.
@@ -436,7 +434,7 @@ Local Hint Resolve elem_of_union.
 
 (* Lemma 3 *)
 Lemma weakly_step_consistent_general `{Policy domain} `{ViewPartition domain} (s t : state) (a : action) ls (u: domain) : weakly_step_consistent -> locally_respects_policy ->
-  view_partition_general (sources (a::ls) u) s t 
+  view_partition_general (sources (a::ls) u) s t
   -> view_partition_general (sources ls u) (step s a) (step t a).
 Proof.
   intros WSC LRP P v vIn.
@@ -444,12 +442,12 @@ Proof.
   unfold locally_respects_policy in LRP.
   destruct (decide (policy (dom a) v)).
   (* Case [dom a ~> v] *)
-  apply WSC; apply P. auto. 
-  (* we need to show that [dom a ∈ sources (a::ls) v] *)  
+  apply WSC; apply P. auto.
+  (* we need to show that [dom a ∈ sources (a::ls) v] *)
   simpl. exists_inside v. apply elem_of_union. right. auto.  apply elem_of_singleton; trivial.
   (* Case [dom a ~/> v] *)
   transitivity s. symmetry. apply LRP; assumption.
-  transitivity t. apply P. auto. 
+  transitivity t. apply P. auto.
   apply LRP; assumption.
 Qed.
 
@@ -476,14 +474,14 @@ Proof.
   induction ls; intros s t.
   simpl. intro A. apply (A u). apply elem_of_singleton; reflexivity.
   intro VPG. simpl. unfold sources. fold (sources (a::ls) u).
-  
+
   destruct (decide _).
   (** Case [dom a ∈ sources (a::ls) u] *)
   simpl. apply IHls. apply weakly_step_consistent_general; auto.
   (** Case [dom a ∉ sources (a::ls) u] *)
-  apply IHls. symmetry. transitivity t. 
+  apply IHls. symmetry. transitivity t.
   - intros v vIn. symmetry. apply VPG. apply sources_mon; exact vIn.
-  - apply locally_respects_gen; try(assumption). 
+  - apply locally_respects_gen; try(assumption).
 Qed.
 
 
@@ -503,7 +501,7 @@ Proof. intro policyA.
   unfold view_partition. unfold RMA_partition; simpl. intros n L.
   destruct (decide (contents (step s a) n = contents s n)) as [E1 | NE1].
   destruct (decide (contents (step t a) n = contents t n)) as [E2 | NE2].
-  (* Case [contents (step s a) n = contents s n /\ contents (step t a) n = contents t n] *) 
+  (* Case [contents (step s a) n = contents s n /\ contents (step t a) n = contents t n] *)
   rewrite E1, E2. apply A1; assumption.
   (* Case [contents (step t a) n ≠ contents t n] *)
   apply rma2; [ | right]; assumption.
diff --git a/_CoqProject b/_CoqProject
index 8c6cef3..df095da 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,2 +1,3 @@
--R . ""
+-R . NI
 Rushby.v
+ArrayMachine.v
\ No newline at end of file
diff --git a/Mealy.v b/experimental/Mealy.v
similarity index 100%
rename from Mealy.v
rename to experimental/Mealy.v
diff --git a/MealySync.v b/experimental/MealySync.v
similarity index 100%
rename from MealySync.v
rename to experimental/MealySync.v
diff --git a/Monoids.v b/experimental/Monoids.v
similarity index 100%
rename from Monoids.v
rename to experimental/Monoids.v
diff --git a/Policy.v b/experimental/Policy.v
similarity index 100%
rename from Policy.v
rename to experimental/Policy.v
diff --git a/Security.v b/experimental/Security.v
similarity index 100%
rename from Security.v
rename to experimental/Security.v
diff --git a/ViewPartition.v b/experimental/ViewPartition.v
similarity index 100%
rename from ViewPartition.v
rename to experimental/ViewPartition.v