diff --git a/example/comparable.msph b/example/comparable.msph
new file mode 100644
index 0000000..2f73457
--- /dev/null
+++ b/example/comparable.msph
@@ -0,0 +1,16 @@
+nominal lt
+nominal eq
+nominal gt
+
+type ord = lt | eq | gt
+
+type comparable[t] = {
+	member cmp : t -> ord
+}
+
+
+type integer = {
+	member cmp : integer -> ord
+}
+
+assert integer <: comparable[integer]
diff --git a/example/ex1.msph b/example/ex1.msph
deleted file mode 100644
index 0844c3f..0000000
--- a/example/ex1.msph
+++ /dev/null
@@ -1,4 +0,0 @@
-
-nominal C
-
-
diff --git a/example/ex2.msph b/example/ex2.msph
deleted file mode 100644
index 5b85fdc..0000000
--- a/example/ex2.msph
+++ /dev/null
@@ -1 +0,0 @@
-type A = & C D
diff --git a/example/ex3.msph b/example/ex3.msph
deleted file mode 100644
index 9770336..0000000
--- a/example/ex3.msph
+++ /dev/null
@@ -1,13 +0,0 @@
-
-type X = & C (| D E)
-
-type Y = {
-	member x : X
-	type Z = & X {
- 		type T = C
-		assert C <: D
-	}
-	member r : (box forall S. (=> S Y))
-	member s : C[X, Y, z]
-	member f : -> A B
-}
diff --git a/example/ex4.msph b/example/ex4.msph
deleted file mode 100644
index ffc0174..0000000
--- a/example/ex4.msph
+++ /dev/null
@@ -1,20 +0,0 @@
-nominal M
-nominal N
-nominal O
-nominal P
-
-type A = {
-	member member1: & N M
-	member member2: | M N
-}
-
-type B = forall X. {
-	member member1 : & X A
-}
-
-member outer1 : box {
-	member member1: & B True
-	type T = & B A
-	member member2 : | (& T O) P
-	type S = & B False
-}
diff --git a/example/ex5.msph b/example/ex5.msph
deleted file mode 100644
index 5774e54..0000000
--- a/example/ex5.msph
+++ /dev/null
@@ -1,21 +0,0 @@
-nominal N
-nominal M
-
-
-type T[X, Y] = {
-	// body
-}
-
-type A = T[N, M] // binding X -> N, Y -> M
-type B = T[M, N] // binding X -> M, Y -> N
-
-// converted to
-
-type A = ⟨ X -> N, Y -> M ⟩ {
-	// body
-}
-type B = ⟨ X -> M, Y -> N ⟩ {
-	// body
-}
-
-
diff --git a/example/graph.msph b/example/graph.msph
new file mode 100644
index 0000000..b636f3b
--- /dev/null
+++ b/example/graph.msph
@@ -0,0 +1,10 @@
+type gnode[e] = {
+	member edges : iterable[e]
+}
+
+type gedge[n] = {
+	member src : n
+	member dst : n
+}
+
+type graph[n, e] = (n <: gnode[e]) & (e <: gedge[n])
diff --git a/example/non-parse/ex6.msph b/example/non-parse/ex6.msph
deleted file mode 100644
index afdeccb..0000000
--- a/example/non-parse/ex6.msph
+++ /dev/null
@@ -1,21 +0,0 @@
-type A[X, Y] = {
-	type B[Z] = {
-		mb : X & Z
-	}
-
-	ma : B[Y]
-}
-
-
-m : A[M, N]
-
-
-m : ⟨X -> M, Y -> N⟩ {
-	ma : B[Y]
-}
-
-m : ⟨X -> M, Y -> N⟩ {
-	ma : ⟨Z -> Y⟩  {
-		mb : X & Z
-	}
-}
diff --git a/example/subt/rec-lockstep.msph b/example/rec-lockstep.msph
similarity index 100%
rename from example/subt/rec-lockstep.msph
rename to example/rec-lockstep.msph
diff --git a/example/self.msph b/example/self.msph
new file mode 100644
index 0000000..d482e1c
--- /dev/null
+++ b/example/self.msph
@@ -0,0 +1,19 @@
+type Accumulator[Self] = (Self <: Accumulator[Self]) & {
+	member add : Int -> Self
+}
+
+type MyAccum = {
+	member add : Int -> MyAccum
+}
+
+assert MyAccum <: Accumulator[MyAccum]
+
+
+
+
+
+type Acchmmmmulator[Self] = (Self <: Acchmmmmulator[Self]) => {
+	member add : Int -> Self
+}
+
+