diff --git a/CMakeLists.txt b/CMakeLists.txt
index 81de430..f22b1e6 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -27,7 +27,6 @@ set(SPHO_HEADER
 	${SPHO_HEADER_DIR}/err.h
 	${SPHO_HEADER_DIR}/scope.h
 	${SPHO_HEADER_DIR}/spho.h
-	${SPHO_HEADER_DIR}/subt.h
 	${SPHO_HEADER_DIR}/tp.h
 )
 
@@ -35,7 +34,6 @@ set(SPHO_SRC
   ${SRC_DIR}/spho/bind.c
   ${SRC_DIR}/spho/ctx.c
   ${SRC_DIR}/spho/scope.c
-  ${SRC_DIR}/spho/subt.c
   ${SRC_DIR}/spho/tp.c
 )
 
diff --git a/docs/about/formalities.md b/docs/about/formalities.md
index b2b01f1..c2a2472 100644
--- a/docs/about/formalities.md
+++ b/docs/about/formalities.md
@@ -24,36 +24,29 @@ a ∈ opname
 
 ## sappho subtyping rules
 
-```cmath
-// trace pairs: none
+```
 ---- [identity]
 s, γ ⊢ s, δ
 
-// trace pairs: none
 ---- [true-right]
 γ ⊢ true, δ
 
-// trace pairs: none
 ---- [false-left]
 false, γ ⊢ δ
 
-// trace pairs: none
 s, t, γ ⊢ δ
 ---- [conj-left]
 s & t, γ ⊢ δ
 
-// trace pairs: none
 γ ⊢ s, t, δ
 ---- [disj-right]
 γ ⊢ s | t, δ
 
-// trace pairs: none
 s, γ ⊢ δ
 t, γ ⊢ δ
 ---- [disj-left]
 s | t, γ ⊢ δ
 
-// trace pairs: none
 γ ⊢ s, δ
 γ ⊢ t, δ
 ---- [conj-right]
@@ -61,24 +54,24 @@ s | t, γ ⊢ δ
 
 // XXX
 // remove s => t? always make progress
-// trace pairs: none
 s => t, s, t, γ ⊢ δ
 ---- [impl-left]
 s => t, s, γ ⊢ δ
 
-// trace pairs: none
+// discussion about implication below
+// check how "normal sequent calculus handles this"
 s, γ ⊢ t, δ
 ---- [impl-right]
 γ ⊢ s => t, δ
 
+
+
 // box works as a kind of "forall" for concrete types
-// trace pairs: none
 box t, t, γ ⊢ δ
 ---- [box-left]
 box t, γ ⊢ δ
 
 // (.)-- filters the contexts.
-// trace pairs: premise[0] -- conclusion
 γ-- ⊢ t, δ--
 ---- [box-right]
 γ ⊢ box t, δ
@@ -89,7 +82,6 @@ box t, γ ⊢ δ
 // to exclude typedefs like
 // type A = A
 // Or that our cycle detection excludes paths between "identical" states.
-// trace pairs: none
 γ ⊢ expand(a[t..]), δ
 ----
 γ ⊢ a[t..], δ
@@ -100,7 +92,6 @@ a[t..], γ ⊢ δ
 
 
 // member types are filtered according to member name
-// trace pairs: premise[0] -- conclusion
 γ >> m ⊢ δ >> m
 ---- [member]
 γ ⊢ δ
@@ -108,14 +99,11 @@ a[t..], γ ⊢ δ
 
 // foralls are unwrapped and variable substituted with fresh name
 // i.e. we treat the bound variable nominally
-// trace pairs: premise[1] -- conclusion
 n fresh
 γ [n] ⊢ δ [n]
 ---- [forall]
 γ ⊢ δ
 
-// 1 + n! premises
-// trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
 c, γ*  ⊢ a_1, ..., a_n
 ∀ I ⊆ {1, ..., n}.
 	c, γ* ⊢ { a_i | i ∈ I }, δ*
@@ -125,6 +113,7 @@ c, γ*  ⊢ a_1, ..., a_n
 a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
 ```
 
+
 ### context operators
 
 * box filtering
@@ -147,14 +136,6 @@ a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
                  γ [n]              otherwise
 ```
 
-### trace pairs
-Trace pairs are related to cyclic proofs. They identify the pairs of 
-`premise -- conclusion` that are *productive*, i.e. leads to some progress
-making a cycle in the proof tree admissable as a cyclic proof of the nodes in
-the cycle.
-
-The trace pairs are described in the comments for each subtyping rule.
-
 ### Semantic function subtyping
 
 *Here we try to give an intuitive explainer of how to reason about function
diff --git a/include/spho/bind.h b/include/spho/bind.h
index 4e175c3..3cdd75d 100644
--- a/include/spho/bind.h
+++ b/include/spho/bind.h
@@ -31,6 +31,11 @@ struct spho_prebind {
 	struct spho_prebind_pair	*binds;
 };
 
+struct spho_bind {
+	struct spho_prebind	*local;
+	struct spho_bind	*parent;
+};
+
 struct spho_prebind	*spho_prebind_create(struct spho_scope *);
 
 int spho_prebind_undef(struct spho_prebind *, const struct spho_nom *);
@@ -43,12 +48,6 @@ int spho_prebind_member_tp(struct spho_prebind *, const struct spho_nom *,
 
 struct spho_prebind *spho_prebind_dupl(const struct spho_prebind *);
 
-void spho_prebind_free(struct spho_prebind *);
-
-
-struct spho_bind {
-	struct spho_prebind	*loc;
-	struct spho_bind	*parent;
-};
+void spho_prebind_destroy(struct spho_prebind *);
 
 #endif
diff --git a/include/spho/scope.h b/include/spho/scope.h
index ff682c4..a9f7526 100644
--- a/include/spho/scope.h
+++ b/include/spho/scope.h
@@ -122,7 +122,7 @@ struct spho_scope {
 	struct spho_nom_l	noms;
 	struct spho_tp_alloc_l	tps;
 
-	struct spho_prebind	*bind_loc;
+	struct spho_prebind	*bind;
 
 	SLIST_ENTRY(spho_scope)	next;
 };
diff --git a/include/spho/subt.h b/include/spho/subt.h
deleted file mode 100644
index c185107..0000000
--- a/include/spho/subt.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _SPHO_SUBT_H
-#define _SPHO_SUBT_H
-
-#include "spho/bind.h"
-
-#endif /* ifndef _SPHO_SUBT_H */
diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c
index a9dec26..0e3c662 100644
--- a/src/msph/sphophi.c
+++ b/src/msph/sphophi.c
@@ -419,7 +419,7 @@ msph_tree_sphophi_tp_prebind(struct spho_scope *sc,
 		if (HAS_PARAMS(tpdef)) {
 			SPHO_ASSERT(HAS_SCOPE(tpdef));
 			SPHO_ASSERT(SCOPE(tpdef) != NULL);
-			SPHO_ASSERT(SCOPE(tpdef)->bind_loc != NULL);
+			SPHO_ASSERT(SCOPE(tpdef)->bind != NULL);
 
 			STAILQ_FOREACH(name, &tpdef->params, entries) {
 				if (spho_scope_prebind_undef(SCOPE(tpdef),
diff --git a/src/spho/bind.c b/src/spho/bind.c
index fc2258b..714b323 100644
--- a/src/spho/bind.c
+++ b/src/spho/bind.c
@@ -158,7 +158,7 @@ spho_prebind_dupl(const struct spho_prebind *bind)
 }
 
 void
-spho_prebind_free(struct spho_prebind *bind)
+spho_prebind_destroy(struct spho_prebind *bind)
 {
 	free(bind->binds);
 	free(bind);
diff --git a/src/spho/scope.c b/src/spho/scope.c
index da5c679..589b8d7 100644
--- a/src/spho/scope.c
+++ b/src/spho/scope.c
@@ -28,7 +28,7 @@ spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx,
 
 	TAILQ_INIT(&sc->tps);
 
-	sc->bind_loc = NULL;
+	sc->bind = NULL;
 
 	return (0);
 }
@@ -42,9 +42,9 @@ spho_scope_term(struct spho_scope *sc)
 
 	sc->parent = NULL;
 
-	if (sc->bind_loc == NULL)
-		spho_prebind_free(sc->bind_loc);
-	sc->bind_loc = NULL;
+	if (sc->bind == NULL)
+		spho_prebind_destroy(sc->bind);
+	sc->bind = NULL;
 }
 
 struct spho_scope *
@@ -177,7 +177,7 @@ spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr,
 int
 spho_scope_prebind_init(struct spho_scope *sc)
 {
-	if ((sc->bind_loc = spho_prebind_create(sc)) 
+	if ((sc->bind = spho_prebind_create(sc)) 
 	    == NULL) {
 		return (-1);
 	}
@@ -194,7 +194,7 @@ spho_scope_prebind_tp(struct spho_scope *sc, struct spho_nom *nom,
 		return (-1);
 	}
 
-	return (spho_prebind_tp(sc->bind_loc, nom, tp));
+	return (spho_prebind_tp(sc->bind, nom, tp));
 }
 
 int
@@ -206,7 +206,7 @@ spho_scope_prebind_tp_op(struct spho_scope *sc, struct spho_nom *nom,
 		return (-1);
 	}
 
-	return (spho_prebind_tp_op(sc->bind_loc, nom, tp_op));
+	return (spho_prebind_tp_op(sc->bind, nom, tp_op));
 }
 
 int
@@ -217,7 +217,7 @@ spho_scope_prebind_undef(struct spho_scope *sc, struct spho_nom *nom)
 		return (-1);
 	}
 
-	return (spho_prebind_undef(sc->bind_loc, nom));
+	return (spho_prebind_undef(sc->bind, nom));
 }
 
 static int
diff --git a/src/spho/subt.c b/src/spho/subt.c
deleted file mode 100644
index 062e021..0000000
--- a/src/spho/subt.c
+++ /dev/null
@@ -1,205 +0,0 @@
-/*
- * Subtyping
- */
-#include <stdlib.h>
-
-#include "spho/bind.h"
-#include "spho/bind.h"
-#include "spho/spho.h"
-
-#include "spho/subt.h"
-
-struct bound_tp {
-	struct spho_bind		*bind;
-	const struct spho_tp		*tp;
-};
-
-struct seqnt {
-	struct spho_ctx		*ctx;
-
-	size_t			sz;
-	size_t			filled;
-	struct bound_tp		*elms;
-};
-
-struct seqnt_tstl {
-	struct seqnt		left;
-	struct seqnt		right;
-};
-
-
-static struct bound_tp *spho_bound_tp(const struct spho_tp *);
-
-
-/* read scopes and create bound type */
-struct bound_tp *
-spho_bound_tp(const struct spho_tp *tp)
-{
-	struct spho_scope	*sc;
-	struct spho_bind	*bind, *more_bind;
-
-	struct bound_tp	*ret;
-
-	SPHO_PRECOND(tp != NULL);
-	SPHO_PRECOND(tp->sc != NULL);
-	SPHO_PRECOND(tp->sc->bind_loc != NULL);
-
-	sc = tp->sc;
-	bind = NULL;
-
-	if ((ret = calloc(1, sizeof(*ret))) == NULL) {
-		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
-		return (NULL);
-	}
-	ret->tp = tp;
-
-	
-	if ((ret->bind = calloc(1, sizeof(*ret->bind))) == NULL) {
-		SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
-		goto err;
-	}
-
-	/* initialize parent and duplicate scope-local bindings */
-	ret->bind->parent = NULL;
-	if ((ret->bind->loc = spho_prebind_dupl(sc->bind_loc)) == NULL) {
-		goto err;
-	}
-
-	/* iterate up through parent scopes and gather their local bindings */
-	bind = ret->bind;
-	while ((sc = sc->parent) != NULL) {
-		if ((more_bind = calloc(1, sizeof(*more_bind))) == NULL) {
-			SPHO_ERR(sc->ctx, SPHO_ERR_SYS);
-			goto err;
-		}
-		more_bind->parent = NULL;
-		if ((more_bind->loc = spho_prebind_dupl(sc->bind_loc))
-		    == NULL) {
-			goto err;
-		}
-		bind->parent = more_bind;
-		bind = bind->parent;
-	}
-
-	return (ret);
-
-err:
-	while (ret->bind != NULL) {
-		bind = ret->bind;
-		ret->bind = ret->bind->parent;
-
-		spho_prebind_free(bind->loc);
-		free(bind);
-	}
-
-	return (NULL);
-}
-
-static struct seqnt *
-seqnt_alloc(struct spho_ctx *ctx, size_t initsz)
-{
-	struct seqnt *seq;
-	if (initsz == 0)
-		initsz = 32; /* just feels good */
-
-	if ((seq = calloc(1, sizeof(*seq))) == NULL) {
-		SPHO_ERR(ctx, SPHO_ERR_SYS);
-		return (NULL);
-	}
-	seq->ctx = ctx;
-
-	if ((seq->elms = calloc(initsz, sizeof(*seq->elms))) == NULL) {
-		SPHO_ERR(seq->ctx, SPHO_ERR_SYS);
-		goto err;
-	}
-
-	seq->sz = initsz;
-	seq->filled = 0;
-
-	return (seq);
-err:
-	if (seq != NULL) {
-		if (seq->elms != NULL)
-			free(seq->elms);
-		free(seq);
-	}
-
-	return (NULL);
-}
-
-static int
-seqnt_makebig(struct seqnt *seq)
-{
-	size_t		new_sz;
-	struct bound_tp *new_elms;
-
-	SPHO_PRECOND(seq != NULL);
-	SPHO_PRECOND(seq->sz > 0);
-	SPHO_PRECOND(seq->sz <= (SIZE_MAX >> 1));
-	SPHO_PRECOND(seq->elms != NULL);
-
-	new_sz = seq->sz << 1;
-
-	if ((new_elms = realloc(seq->elms, new_sz)) == NULL) {
-		SPHO_ERR(seq->ctx, SPHO_ERR_SYS);
-		return (-1);
-	}
-
-	seq->sz = new_sz;
-	seq->elms = new_elms;
-
-	return (0);
-}
-
-static int
-seqnt_insert_from_ptr(struct seqnt *seq, struct bound_tp *elm)
-{
-	SPHO_PRECOND(seq->filled <= seq->sz);
-
-	if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1))
-		return (-1);
-
-	seq->elms[seq->filled++] = *elm;
-
-	SPHO_POSTCOND(seq->filled <= seq->sz);
-
-	return (0);
-}
-
-static int
-seqnt_insert_bind_tp(struct seqnt *seq, struct spho_bind *elm_bind,
-    struct spho_tp *elm_tp)
-{
-	SPHO_PRECOND(seq->filled <= seq->sz);
-
-	if (seq->filled >= seq->sz && (seqnt_makebig(seq) == -1))
-		return (-1);
-
-	seq->elms[seq->filled++] = (struct bound_tp){ elm_bind, elm_tp };
-
-	SPHO_POSTCOND(seq->filled <= seq->sz);
-
-	return (0);
-}
-
-
-int
-spho_is_subt(struct spho_tp *tp_left, struct spho_tp *tp_right)
-{
-	struct bound_tp *left, *right;
-
-	if ((left = spho_bound_tp(tp_left)) == NULL)
-		return (-1);
-	if ((right = spho_bound_tp(tp_right)) == NULL)
-		return (-1);
-
-	// TODO check well-definedness (e.g. no undefs)
-
-	// XXX skip boxing step
-	
-	// TODO create seqnt and seqnt_tstl
-	// TODO run decider
-
-	return (-1);
-}
-