diff --git a/ArrayMachine.v b/ArrayMachine.v
index b1443ef..9832faf 100644
--- a/ArrayMachine.v
+++ b/ArrayMachine.v
@@ -1,5 +1,5 @@
 Require Import Rushby.
-Require Import list relations collections fin_collections.
+From stdpp Require Import list relations collections fin_collections.
 
 Module ArrayMachine <: Mealy.
 
diff --git a/Mealy.v b/Mealy.v
index 52b325c..83bb023 100644
--- a/Mealy.v
+++ b/Mealy.v
@@ -1,4 +1,4 @@
-Require Import base.
+From stdpp Require Import base.
 Require Import Monoids.
 
 Class Mealy (state action out : Type) := {
diff --git a/MealySync.v b/MealySync.v
index 441a142..58bbb6f 100644
--- a/MealySync.v
+++ b/MealySync.v
@@ -1,5 +1,5 @@
 Require Import Rushby.
-Require Import base.
+From stdpp Require Import base.
 
 Class MSync (state action out : Type) 
   := {
@@ -25,29 +25,24 @@ Section MealyM.
 Variable state action out : Type.
 Variable MM : MSync state action out.
 Variable domain : Type.
-Check Policy.
-Variable P : Policy domain.
-Variable VP : ViewPartition domain.
+Check @Policy.
+Variable P : @Policy action domain.
+Variable VP : @ViewPartition action domain.
 
 
 Definition sync_separation `{Policy action domain} := forall (s : state) (b : action) (a : action),
    ¬ (delayed a s) ∧ (delayed a (step s a))
    → policy (Rushby.dom b) (Rushby.dom a).
 
-Definition sync_interf `{Policy action domain} `{MMs : MMsync state action out}
-
-Class SyncPartition {domain state action out : Type} (MMs : MMsync state action out) {P : Policy domain} {VP : @ViewPartition state domain} :=  { 
-  sync_partitioned : forall s t a,  view_partition (Rushby.dom a) s t  -> (delayed a s <-> delayed a t)
- }.
-
+End MealyM.
 
 Section Unwinding.
 Context {state action out : Type}.
 Context {domain : Type}.
 Context {P : @Policy action domain}.
 Context {VP : @ViewPartition state domain}.
-Context {MMs : MMsync state action out}.
-Definition MM := underlyingM.
+Context {MMs : MSync state action out}.
+Definition MM := msync_mealy.
 Definition N := (@MMsync_is_MM domain state action out MMs).
 
 Context {OC : @OutputConsistent _ _ _ MM domain P VP}.
diff --git a/Monoids.v b/Monoids.v
index 912f4eb..f7e5dd4 100644
--- a/Monoids.v
+++ b/Monoids.v
@@ -1,4 +1,4 @@
-Require Import base.
+From stdpp Require Import base.
 
 Class Monad M {ret : MRet M} {bind : MBind M} :=
   { ret_unit_1 : forall {A} (m : M A) , m ≫= mret = m
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..344b193
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+Formalisation of ["Noninterference, Transitivity, and Channel-Control Security Policies"](http://www.csl.sri.com/papers/csl-92-2/) by John Rushby.
+
+Requires [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp).
+
+The proofs are in `Rushby.v`.