diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs
index 3d9bd82..85cd9f0 100644
--- a/bidir/src/bidir.rs
+++ b/bidir/src/bidir.rs
@@ -2,7 +2,7 @@ use anyhow::{bail, Result};
 
 use crate::DEPTH;
 
-use crate::data::FreeVar;
+use crate::data::{FreeVar, Monotype};
 use crate::{
   data::{Context, ContextEntry, Term, Type},
   gensym::gensym_prefix,
@@ -10,12 +10,11 @@ use crate::{
 
 // Figure 8. Applying a context, as a substitution, to a type
 
-#[trace]
 pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
   match ty {
     Type::Existential(a) => match ctx.lookup_existential(a) {
-      Some(Some(m)) => Ok(m.into_poly()),
-      Some(None) => Ok(Type::Existential(a.clone())),
+      Some((_, Some(m))) => Ok(m.into_poly()),
+      Some((_, None)) => Ok(Type::Existential(a.clone())),
       None => bail!("existential variable {a} doesn't exist in context"),
     },
 
@@ -38,22 +37,12 @@ pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
     (Type::Unit, Type::Unit) => Ok(ctx.clone()),
 
     // <:Var rule
-    (Type::Var(x), Type::Var(y)) if x == y => {
-      // Ensure that the name exists in the context
-      if ctx.lookup_type(x).is_none() {
-        bail!("name {x} not in context");
-      }
-
-      Ok(ctx.clone())
-    }
+    (Type::Var(x), Type::Var(y)) if x == y && ctx.lookup_type(x).is_some() => Ok(ctx.clone()),
 
     // <:Exvar rule
-    (Type::Existential(x), Type::Existential(y)) if x == y => {
-      // Ensure that the name exists in the context
-      if ctx.lookup_existential(x).is_none() {
-        bail!("name {x} not in context");
-      }
-
+    (Type::Existential(x), Type::Existential(y))
+      if x == y && ctx.lookup_existential(x).is_some() =>
+    {
       Ok(ctx.clone())
     }
 
@@ -90,9 +79,21 @@ pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result<Context>
   match ty_a {
     // InstLReach rule
     Type::Existential(b) if ctx.has_existential(a) && ctx.has_existential(b) => {
-      // TODO: WTF?
-      todo!()
+      let mut new_ctx = ctx.clone();
+      {
+        let b_entry = new_ctx
+          .0
+          .iter_mut()
+          .find(|entry| matches!(entry, ContextEntry::ExistentialVar(x) if x == b))
+          .expect("should exist");
+
+        *b_entry =
+          ContextEntry::ExistentialSolved(b.to_owned(), Monotype::Existential(a.to_owned()));
+      }
+
+      Ok(new_ctx)
     }
+
     Type::Existential(b) => todo!(),
 
     Type::Unit => todo!(),
@@ -134,13 +135,11 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
 pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
   match term {
     // Var rule
-    Term::Var(name) => {
-      let ty = match ctx.lookup_type(name) {
-        Some(v) => v,
-        None => bail!("could not find name {name}"),
-      };
+    Term::Var(name) if ctx.has_type(name) => {
+      let (_, ty) = ctx.lookup_type(name).unwrap();
       Ok((ty, ctx.clone()))
     }
+    Term::Var(name) => bail!("could not find name {name}"),
 
     // 1I⇒ rule
     Term::Unit => Ok((Type::Unit, ctx.clone())),
diff --git a/bidir/src/data.rs b/bidir/src/data.rs
index bcf2df1..5f5cdfd 100644
--- a/bidir/src/data.rs
+++ b/bidir/src/data.rs
@@ -1,8 +1,11 @@
-use std::hash::Hash;
+use std::{
+  fmt::{self, write},
+  hash::Hash,
+};
 
 use im::{HashSet, Vector};
 
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub enum Term {
   Unit,
   Var(String),
@@ -11,7 +14,19 @@ pub enum Term {
   Annot(Box<Term>, Type),
 }
 
-#[derive(Debug, Clone)]
+impl fmt::Debug for Term {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::Unit => write!(f, "unit"),
+      Self::Var(arg0) => write!(f, "`{}", arg0),
+      Self::Lam(arg0, arg1) => write!(f, "λ{}.{:?}", arg0, arg1),
+      Self::App(arg0, arg1) => write!(f, "({:?} · {:?})", arg0, arg1),
+      Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1),
+    }
+  }
+}
+
+#[derive(Clone)]
 pub enum Type {
   Unit,
   Var(String),
@@ -20,6 +35,18 @@ pub enum Type {
   Arrow(Box<Type>, Box<Type>),
 }
 
+impl fmt::Debug for Type {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::Unit => write!(f, "𝟙"),
+      Self::Var(arg0) => write!(f, "`α-{}", arg0),
+      Self::Existential(arg0) => write!(f, "`α\u{0302}-{}", arg0),
+      Self::Polytype(arg0, arg1) => write!(f, "(∀{}.{:?})", arg0, arg1),
+      Self::Arrow(arg0, arg1) => write!(f, "({:?} → {:?})", arg0, arg1),
+    }
+  }
+}
+
 impl Type {
   pub fn into_mono(&self) -> Option<Monotype> {
     match self {
@@ -90,7 +117,7 @@ impl Monotype {
   }
 }
 
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub enum ContextEntry {
   TypeVar(String),
   TermAnnot(String, Type),
@@ -99,6 +126,18 @@ pub enum ContextEntry {
   Marker(String),
 }
 
+impl fmt::Debug for ContextEntry {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    match self {
+      Self::TypeVar(arg0) => write!(f, "`{}", arg0),
+      Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1),
+      Self::ExistentialVar(arg0) => write!(f, "`{}", arg0),
+      Self::ExistentialSolved(arg0, arg1) => write!(f, "{:?} = {:?}", arg0, arg1),
+      Self::Marker(arg0) => write!(f, "▶{}", arg0),
+    }
+  }
+}
+
 #[derive(Debug, Clone)]
 pub enum CompleteContextEntry {
   TypeVar(String),
@@ -107,8 +146,19 @@ pub enum CompleteContextEntry {
   Marker(String),
 }
 
-#[derive(Debug, Clone, Default)]
-pub struct Context(Vector<ContextEntry>);
+#[derive(Clone, Default)]
+pub struct Context(pub(crate) Vector<ContextEntry>);
+
+impl fmt::Debug for Context {
+  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+    f.write_str("Γ")?;
+    for rule in self.0.iter() {
+      f.write_str(", ")?;
+      rule.fmt(f)?;
+    }
+    Ok(())
+  }
+}
 
 impl Context {
   pub fn add(&self, entries: Vec<ContextEntry>) -> Context {
@@ -119,12 +169,16 @@ impl Context {
     new_ctx
   }
 
-  /// Looks up a polytype by name
-  pub fn lookup_type(&self, name: impl AsRef<str>) -> Option<Type> {
-    self.0.iter().find_map(|entry| match entry {
-      ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some(t.clone()),
-      _ => None,
-    })
+  /// Looks up a polytype by name, also returning an index
+  pub fn lookup_type(&self, name: impl AsRef<str>) -> Option<(usize, Type)> {
+    self
+      .0
+      .iter()
+      .enumerate()
+      .find_map(|(i, entry)| match entry {
+        ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some((i, t.clone())),
+        _ => None,
+      })
   }
 
   #[inline]
@@ -136,12 +190,16 @@ impl Context {
   /// - Returns Some(Some(t)) if solved
   /// - Returns Some(None) if exists but unsolved
   /// - Returns None if not found
-  pub fn lookup_existential(&self, name: impl AsRef<str>) -> Option<Option<Monotype>> {
-    self.0.iter().find_map(|entry| match entry {
-      ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some(None),
-      ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some(Some(t.clone())),
-      _ => None,
-    })
+  pub fn lookup_existential(&self, name: impl AsRef<str>) -> Option<(usize, Option<Monotype>)> {
+    self
+      .0
+      .iter()
+      .enumerate()
+      .find_map(|(i, entry)| match entry {
+        ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some((i, None)),
+        ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some((i, Some(t.clone()))),
+        _ => None,
+      })
   }
 
   #[inline]
diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs
index 1efff03..ab1b67b 100644
--- a/bidir/src/tests.rs
+++ b/bidir/src/tests.rs
@@ -1,7 +1,7 @@
 use anyhow::{bail, Result};
 
 use crate::{
-  bidir::synthesize,
+  bidir::{app_ctx, synthesize},
   data::{Context, Term},
 };
 
@@ -15,7 +15,9 @@ macro_rules! id_term {
 fn test_id() -> Result<()> {
   let id = id_term!();
   let ctx = Context::default();
-  bail!("Result: {:?}", synthesize(&ctx, &id));
+  let (ty, out_ctx) = synthesize(&ctx, &id)?;
+  let ty2 = app_ctx(&out_ctx, &ty)?;
+  println!("Result: {:?}", ty2);
   Ok(())
 }