diff --git a/src/haz3lcore/VarMap.re b/src/haz3lcore/VarMap.re
index 85bdd70980..394969139a 100644
--- a/src/haz3lcore/VarMap.re
+++ b/src/haz3lcore/VarMap.re
@@ -19,6 +19,9 @@ let concat = (ctx, new_ctx) => new_ctx @ ctx;
 
 let lookup = (ctx, x) => List.assoc_opt(x, ctx);
 
+let lookup_all = (ctx, x) =>
+  List.fold_left((vs, (tok, v)) => {tok == x ? [v, ...vs] : vs}, [], ctx);
+
 let contains = (ctx, x) => List.mem_assoc(x, ctx);
 
 let map = (f, xs) => List.map(((x, _) as xa) => (x, f(xa)), xs);
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 86e4a8ca34..bd7aa246e4 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -38,7 +38,8 @@ type info_pat = {
   term: Term.UPat.t,
   mode: Typ.mode,
   self: Typ.self,
-  ctx: Ctx.t // TODO: detect in-pattern shadowing
+  ctx: Ctx.t, // TODO: detect in-pattern shadowing
+  body_ids: list(Id.t),
 };
 
 /* (Syntactic) Types are assigned their corresponding semantic type. */
@@ -160,6 +161,90 @@ let is_error = (ci: t): bool => {
   };
 };
 
+type usage_info = (Token.t, list(Id.t));
+let binding_uses = (ci: t, info_map: map): list(usage_info) => {
+  switch (ci) {
+  | InfoPat({term, body_ids, _}) =>
+    let bindings = List.sort_uniq(compare, Term.UPat.get_all_bindings(term));
+    let exps_to_search: list(info_exp) =
+      List.fold_left(
+        (exps, id) => {
+          switch (Id.Map.find_opt(id, info_map)) {
+          | Some(InfoExp(info_body)) => [info_body, ...exps]
+          | _ => exps
+          }
+        },
+        [],
+        body_ids,
+      );
+    let empty_bindings_map: list(usage_info) =
+      List.map(var => (var, []), bindings);
+    let bindings_map =
+      List.fold_left(
+        (binding_map: list(usage_info), info_exp: info_exp) => {
+          let updated_map: list(usage_info) =
+            List.map(
+              (usage_pair: usage_info) => {
+                let (var, ids) = usage_pair;
+                let new_ids: list(Id.t) =
+                  List.map(
+                    (item: Ctx.co_item) => {item.id},
+                    List.flatten(VarMap.lookup_all(info_exp.free, var)),
+                  );
+                print_string("co_ctx | ");
+                let _ =
+                  List.map(
+                    coctx_pair => {
+                      let (var, co_items) = coctx_pair;
+                      print_string(var);
+                      print_string(":[");
+                      let _ =
+                        List.map(
+                          (co_it: Ctx.co_item) => {
+                            print_int(co_it.id);
+                            print_string(",");
+                          },
+                          co_items,
+                        );
+                      print_string("]; ");
+                    },
+                    info_exp.free,
+                  );
+                let all_ids: list(Id.t) =
+                  List.sort_uniq(compare, new_ids @ ids);
+                let pair: (Token.t, list(Id.t)) = (var, all_ids);
+                pair;
+              },
+              binding_map,
+            );
+          updated_map;
+        },
+        empty_bindings_map,
+        exps_to_search,
+      );
+    let _ =
+      List.map(
+        (usage_pair: usage_info) => {
+          let (var, ids) = usage_pair;
+          print_string(var);
+          print_string(": ");
+          let _ =
+            List.map(
+              id => {
+                print_int(id);
+                print_string(", ");
+              },
+              ids,
+            );
+          print_newline();
+        },
+        bindings_map,
+      );
+    bindings_map;
+  | _ => []
+  };
+};
+
 /* Determined the type of an expression or pattern 'after hole wrapping';
    that is, all ill-typed terms are considered to be 'wrapped in
    non-empty holes', i.e. assigned Unknown type. */
@@ -226,12 +311,13 @@ let add_info = (ids, info: 'a, m: Ptmap.t('a)) =>
   |> List.fold_left(Id.Map.disj_union, m);
 
 let extend_let_def_ctx =
-    (ctx: Ctx.t, pat: Term.UPat.t, pat_ctx: Ctx.t, def: Term.UExp.t) =>
+    (ctx: Ctx.t, pat: Term.UPat.t, pat_ctx: Ctx.t, def: Term.UExp.t)
+    : (Ctx.t, bool) =>
   if (Term.UPat.is_tuple_of_arrows(pat)
       && Term.UExp.is_tuple_of_functions(def)) {
-    VarMap.concat(ctx, pat_ctx);
+    (VarMap.concat(ctx, pat_ctx), true);
   } else {
-    ctx;
+    (ctx, false);
   };
 
 let typ_exp_binop_bin_int: Term.UExp.op_bin_int => Typ.t =
@@ -415,7 +501,8 @@ and uexp_to_info_map =
     );
   | Fun(pat, body) =>
     let (mode_pat, mode_body) = Typ.matched_arrow_mode(mode);
-    let (ty_pat, ctx_pat, m_pat) = upat_to_info_map(~mode=mode_pat, pat);
+    let (ty_pat, ctx_pat, m_pat) =
+      upat_to_info_map(~mode=mode_pat, ~body_ids=body.ids, pat);
     let ctx_body = VarMap.concat(ctx, ctx_pat);
     let (ty_body, free_body, m_body) =
       uexp_to_info_map(~ctx=ctx_body, ~mode=mode_body, body);
@@ -425,25 +512,49 @@ and uexp_to_info_map =
       union_m([m_pat, m_body]),
     );
   | Let(pat, def, body) =>
-    let (ty_pat, ctx_pat, _m_pat) = upat_to_info_map(~mode=Syn, pat);
-    let def_ctx = extend_let_def_ctx(ctx, pat, ctx_pat, def);
+    let (ty_pat, ctx_pat, _m_pat) =
+      upat_to_info_map(~mode=Syn, ~body_ids=body.ids @ def.ids, pat);
+    let (def_ctx, is_rec) = extend_let_def_ctx(ctx, pat, ctx_pat, def);
+    // use this ^^ to determine if recursive let or not
     let (ty_def, free_def, m_def) =
       uexp_to_info_map(~ctx=def_ctx, ~mode=Ana(ty_pat), def);
     /* Analyze pattern to incorporate def type into ctx */
-    let (_, ctx_pat_ana, m_pat) = upat_to_info_map(~mode=Ana(ty_def), pat);
+    let pat_body_ids =
+      if (is_rec) {
+        body.ids @ def.ids;
+      } else {
+        body.ids;
+      };
+    let (_, ctx_pat_ana, m_pat) =
+      upat_to_info_map(~mode=Ana(ty_def), ~body_ids=pat_body_ids, pat);
     let ctx_body = VarMap.concat(ctx, ctx_pat_ana);
     let (ty_body, free_body, m_body) =
       uexp_to_info_map(~ctx=ctx_body, ~mode, body);
     add(
       ~self=Just(ty_body),
-      ~free=Ctx.union([free_def, Ctx.subtract_typ(ctx_pat_ana, free_body)]),
+      ~free=
+        Ctx.union([
+          free_def,
+          Ctx.subtract_typ(
+            def_ctx,
+            Ctx.subtract_typ(ctx_pat_ana, free_body),
+          ),
+        ]),
       union_m([m_pat, m_def, m_body]),
     );
   | Match(scrut, rules) =>
     let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut);
     let (pats, branches) = List.split(rules);
     let pat_infos =
-      List.map(upat_to_info_map(~mode=Typ.Ana(ty_scrut)), pats);
+      List.mapi(
+        (i, p) =>
+          upat_to_info_map(
+            ~mode=Typ.Ana(ty_scrut),
+            ~body_ids=List.nth(branches, i).ids,
+            p,
+          ),
+        pats,
+      );
     let branch_infos =
       List.map2(
         (branch, (_, ctx_pat, _)) =>
@@ -459,9 +570,17 @@ and uexp_to_info_map =
       );
     let pat_ms = List.map(((_, _, m)) => m, pat_infos);
     let branch_ms = List.map(((_, _, m)) => m, branch_infos);
-    let branch_frees = List.map(((_, free, _)) => free, branch_infos);
+    let branch_frees =
+      List.map2(
+        ((_, body_free, _), (_, ctx_pat, _)) => {
+          Ctx.subtract_typ(ctx_pat, body_free)
+        },
+        branch_infos,
+        pat_infos,
+      );
     let self = Typ.Joined(Fun.id, branch_sources);
-    let free = Ctx.union([free_scrut] @ branch_frees);
+    /* let free = Ctx.union([free_scrut] @ branch_frees); */
+    let free = Ctx.union([free_scrut, ...branch_frees]);
     add(~self, ~free, union_m([m_scrut] @ pat_ms @ branch_ms));
   };
 }
@@ -469,6 +588,7 @@ and upat_to_info_map =
     (
       ~ctx=Ctx.empty,
       ~mode: Typ.mode=Typ.Syn,
+      ~body_ids: list(Id.t)=[Id.invalid],
       {ids, term} as upat: Term.UPat.t,
     )
     : (Typ.t, Ctx.t, map) => {
@@ -476,7 +596,7 @@ and upat_to_info_map =
   let add = (~self, ~ctx, m) => (
     typ_after_fix(mode, self),
     ctx,
-    add_info(ids, InfoPat({cls, self, mode, ctx, term: upat}), m),
+    add_info(ids, InfoPat({cls, self, mode, ctx, body_ids, term: upat}), m),
   );
   let atomic = self => add(~self, ~ctx, Id.Map.empty);
   let unknown = Typ.Just(Unknown(SynSwitch));
@@ -503,7 +623,8 @@ and upat_to_info_map =
     let (ctx, infos) =
       List.fold_left2(
         ((ctx, infos), e, mode) => {
-          let (_, ctx, _) as info = upat_to_info_map(~mode, ~ctx, e);
+          let (_, ctx, _) as info =
+            upat_to_info_map(~mode, ~ctx, ~body_ids, e);
           (ctx, infos @ [info]);
         },
         (ctx, []),
@@ -520,15 +641,17 @@ and upat_to_info_map =
         )
       | Some(ty) => Just(List(ty))
       };
-    let info: t = InfoPat({cls, self, mode, ctx, term: upat});
+    let info: t = InfoPat({cls, self, mode, body_ids, ctx, term: upat});
     let m = union_m(List.map(((_, _, m)) => m, infos));
     /* Add an entry for the id of each comma tile */
     let m = List.fold_left((m, id) => Id.Map.add(id, info, m), m, ids);
     (typ_after_fix(mode, self), ctx, m);
   | Cons(hd, tl) =>
     let mode_elem = Typ.matched_list_mode(mode);
-    let (ty, ctx, m_hd) = upat_to_info_map(~ctx, ~mode=mode_elem, hd);
-    let (_, ctx, m_tl) = upat_to_info_map(~ctx, ~mode=Ana(List(ty)), tl);
+    let (ty, ctx, m_hd) =
+      upat_to_info_map(~ctx, ~mode=mode_elem, ~body_ids, hd);
+    let (_, ctx, m_tl) =
+      upat_to_info_map(~ctx, ~mode=Ana(List(ty)), ~body_ids, tl);
     add(~self=Just(List(ty)), ~ctx, union_m([m_hd, m_tl]));
   | Tag(name) =>
     switch (BuiltinADTs.get_tag_typ(name)) {
@@ -549,7 +672,8 @@ and upat_to_info_map =
     let (ctx, infos) =
       List.fold_left2(
         ((ctx, infos), e, mode) => {
-          let (_, ctx, _) as info = upat_to_info_map(~mode, ~ctx, e);
+          let (_, ctx, _) as info =
+            upat_to_info_map(~mode, ~ctx, ~body_ids, e);
           (ctx, infos @ [info]);
         },
         (ctx, []),
@@ -560,18 +684,21 @@ and upat_to_info_map =
     let m = union_m(List.map(((_, _, m)) => m, infos));
     add(~self, ~ctx, m);
   | Parens(p) =>
-    let (ty, ctx, m) = upat_to_info_map(~ctx, ~mode, p);
+    let (ty, ctx, m) = upat_to_info_map(~ctx, ~mode, ~body_ids, p);
     add(~self=Just(ty), ~ctx, m);
   | Ap(fn, arg) =>
     /* Contructor application */
     /* Function position mode Ana(Hole->Hole) instead of Syn */
-    let (ty_fn, ctx, m_fn) = upat_to_info_map(~ctx, ~mode=Typ.ap_mode, fn);
+    let (ty_fn, ctx, m_fn) =
+      upat_to_info_map(~ctx, ~mode=Typ.ap_mode, ~body_ids, fn);
     let (ty_in, ty_out) = Typ.matched_arrow(ty_fn);
-    let (_, ctx, m_arg) = upat_to_info_map(~ctx, ~mode=Ana(ty_in), arg);
+    let (_, ctx, m_arg) =
+      upat_to_info_map(~ctx, ~mode=Ana(ty_in), ~body_ids, arg);
     add(~self=Just(ty_out), ~ctx, union_m([m_fn, m_arg]));
   | TypeAnn(p, ty) =>
     let (ty_ann, m_typ) = utyp_to_info_map(ty);
-    let (_ty, ctx, m) = upat_to_info_map(~ctx, ~mode=Ana(ty_ann), p);
+    let (_ty, ctx, m) =
+      upat_to_info_map(~ctx, ~mode=Ana(ty_ann), ~body_ids, p);
     add(~self=Just(ty_ann), ~ctx, union_m([m, m_typ]));
   };
 }
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 90d9d785d1..3d5842bd46 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -319,6 +319,29 @@ module UPat = {
       }
     };
   };
+
+  let rec get_all_bindings = (pat: t) => {
+    switch (pat.term) {
+    | Var(x) => [x]
+    | Parens(pat)
+    | TypeAnn(pat, _) => get_all_bindings(pat)
+    | Cons(pat1, pat2)
+    | Ap(pat1, pat2) =>
+      List.append(get_all_bindings(pat1), get_all_bindings(pat2))
+    | ListLit(pats)
+    | Tuple(pats) => List.flatten(List.map(get_all_bindings, pats))
+    | Invalid(_)
+    | EmptyHole
+    | MultiHole(_)
+    | Wild
+    | Int(_)
+    | Float(_)
+    | Bool(_)
+    | String(_)
+    | Triv
+    | Tag(_) => []
+    };
+  };
 };
 
 module UExp = {
diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
index 96f1de4183..7e33091e16 100644
--- a/src/haz3lweb/view/Cell.re
+++ b/src/haz3lweb/view/Cell.re
@@ -155,6 +155,18 @@ let test_result_layer =
   );
 };
 
+let get_usage_ids = (zipper, info_map) => {
+  /* bad style, does reason have let*? */
+  switch (Haz3lcore.Indicated.index(zipper)) {
+  | Some(index) =>
+    switch (Haz3lcore.Id.Map.find_opt(index, info_map)) {
+    | Some(ci) => Haz3lcore.Statics.binding_uses(ci, info_map)
+    | None => []
+    }
+  | None => []
+  };
+};
+
 let deco =
     (
       ~zipper,
@@ -168,6 +180,16 @@ let deco =
       ~color_highlighting: option(ColorSteps.colorMap),
     ) => {
   let unselected = Zipper.unselect_and_zip(zipper);
+  let use_ids = get_usage_ids(zipper, info_map);
+  let use_highlights =
+    List.flatten(
+      List.map(
+        ((_tok, ids): Haz3lcore.Statics.usage_info) => {
+          List.map(id => (id, "orange"), ids)
+        },
+        use_ids,
+      ),
+    );
   module Deco =
     Deco.Deco({
       let font_metrics = font_metrics;
@@ -179,6 +201,7 @@ let deco =
       let tiles = TileMap.mk(unselected);
     });
   let decos = selected ? Deco.all(zipper, segment) : Deco.err_holes(zipper);
+  let decos = decos @ Deco.color_highlights(use_highlights);
   let decos =
     switch (test_results) {
     | None => decos
diff --git a/src/haz3lweb/view/CursorInspector.re b/src/haz3lweb/view/CursorInspector.re
index 2bcd1e4017..d18ccd613e 100644
--- a/src/haz3lweb/view/CursorInspector.re
+++ b/src/haz3lweb/view/CursorInspector.re
@@ -250,7 +250,24 @@ let view =
     | Some(index) =>
       switch (Haz3lcore.Id.Map.find_opt(index, info_map)) {
       | Some(ci) =>
-        inspector_view(~inject, ~settings, ~show_lang_doc, index, ci)
+        let _ =
+          List.map(
+            usage => {
+              print_string(fst(usage));
+              print_string(": ");
+              let _ =
+                List.map(
+                  id => {
+                    print_int(id);
+                    print_string(", ");
+                  },
+                  snd(usage),
+                );
+              print_newline();
+            },
+            Haz3lcore.Statics.binding_uses(ci, info_map),
+          );
+        inspector_view(~inject, ~settings, ~show_lang_doc, index, ci);
       | None =>
         div(
           ~attr=clss(["cursor-inspector"]),