diff --git a/Cargo.lock b/Cargo.lock
index a76f56d..896f5fa 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -19,6 +19,7 @@ name = "bidir"
 version = "0.1.0"
 dependencies = [
  "anyhow",
+ "dashmap",
  "im",
  "lazy_static",
  "parking_lot",
@@ -46,6 +47,25 @@ version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
+[[package]]
+name = "dashmap"
+version = "5.5.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "978747c1d849a7d2ee5e8adc0159961c48fb7e5db2f06af6723b80123bb53856"
+dependencies = [
+ "cfg-if",
+ "hashbrown",
+ "lock_api",
+ "once_cell",
+ "parking_lot_core",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.14.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
+
 [[package]]
 name = "im"
 version = "15.1.0"
@@ -82,6 +102,12 @@ dependencies = [
  "scopeguard",
 ]
 
+[[package]]
+name = "once_cell"
+version = "1.18.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d"
+
 [[package]]
 name = "parking_lot"
 version = "0.12.1"
diff --git a/bidir/Cargo.toml b/bidir/Cargo.toml
index 0b501d2..e9d21a8 100644
--- a/bidir/Cargo.toml
+++ b/bidir/Cargo.toml
@@ -7,6 +7,7 @@ edition = "2021"
 
 [dependencies]
 anyhow = "1.0.75"
+dashmap = "5.5.3"
 im = "15.1.0"
 lazy_static = "1.4.0"
 parking_lot = "0.12.1"
diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs
index 85cd9f0..e309f37 100644
--- a/bidir/src/bidir.rs
+++ b/bidir/src/bidir.rs
@@ -2,11 +2,8 @@ use anyhow::{bail, Result};
 
 use crate::DEPTH;
 
-use crate::data::{FreeVar, Monotype};
-use crate::{
-  data::{Context, ContextEntry, Term, Type},
-  gensym::gensym_prefix,
-};
+use crate::data::{Context, ContextEntry, FreeVar, Monotype, Term, Type};
+use crate::gensym::gensym_existential;
 
 // Figure 8. Applying a context, as a substitution, to a type
 
@@ -31,8 +28,8 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
 
 /// Under input context Γ , type A is a subtype of B, with output context ∆
 #[trace]
-pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
-  match (a, b) {
+pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
+  match (left, right) {
     // <:Unit rule
     (Type::Unit, Type::Unit) => Ok(ctx.clone()),
 
@@ -47,7 +44,9 @@ pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
     }
 
     (Type::Existential(a), ty_a)
-      if !b.free_vars().contains(&FreeVar::Existential(a.to_string()))
+      if !right
+        .free_vars()
+        .contains(&FreeVar::Existential(a.to_string()))
         && ctx.lookup_existential(a).is_some() =>
     {
       let ctx_delta = instantiate_left(ctx, a, ty_a)?;
@@ -68,7 +67,7 @@ pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result<Context> {
     (Type::Arrow(_, _), Type::Polytype(_, _)) => todo!(),
     (Type::Arrow(_, _), Type::Arrow(_, _)) => todo!(),
 
-    _ => bail!("subtyping relation failed between {a:?} and {b:?} (ctx = {ctx:?})"),
+    _ => bail!("subtyping relation failed between {left:?} and {right:?} (ctx = {ctx:?})"),
   }
 }
 
@@ -160,8 +159,8 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
     // > not place a marker before ^α, because ^α and ^β appear in the output type
     // > (λx. e ⇒ ^α → ^β).
     Term::Lam(x, e) => {
-      let ex_a_s = gensym_prefix("ex");
-      let ex_b_s = gensym_prefix("ex");
+      let ex_a_s = gensym_existential();
+      let ex_b_s = gensym_existential();
       let ex_a = Type::Existential(ex_a_s.clone());
       let ex_b = Type::Existential(ex_b_s.clone());
       let aug_ctx = ctx.add(vec![
diff --git a/bidir/src/gensym.rs b/bidir/src/gensym.rs
index 738ff46..85359d4 100644
--- a/bidir/src/gensym.rs
+++ b/bidir/src/gensym.rs
@@ -1,18 +1,35 @@
+use dashmap::DashMap;
 use lazy_static::lazy_static;
-use parking_lot::Mutex;
 
-lazy_static! {
-  static ref CTR: Mutex<usize> = Mutex::new(0);
+thread_local! {
+  static CTRMAP: DashMap<&'static str, usize> = DashMap::new();
 }
 
-pub fn gensym() -> String {
-  gensym_prefix("var")
+const EXISTENTIALS: [&'static str; 24] = [
+  "α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο", "π", "ρ", "σ", "τ",
+  "υ", "φ", "χ", "ψ", "ω",
+];
+
+const TYPEVARS: [&'static str; 26] = [
+  "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O", "P", "Q", "R", "S",
+  "T", "U", "V", "W", "X", "Y", "Z",
+];
+
+pub fn gensym_existential() -> String {
+  let result = idx("existential");
+  format!("{}\u{0302}", EXISTENTIALS[result])
 }
 
-pub fn gensym_prefix(prefix: impl AsRef<str>) -> String {
-  let mut g = CTR.lock();
-  let ctr = *g;
-  *g += 1;
-  drop(g);
-  format!("{}{}", prefix.as_ref(), ctr)
+pub fn gensym_type() -> String {
+  let result = idx("existential");
+  format!("{}\u{0302}", TYPEVARS[result])
+}
+
+fn idx(ty: &'static str) -> usize {
+  CTRMAP.with(|ctrmap| {
+    let mut g = ctrmap.entry(ty).or_insert(0);
+    let ctr = *g;
+    *g += 1;
+    ctr
+  })
 }