diff --git a/src/lib.rs b/src/lib.rs
index 996101cfb..fff069c73 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -121,7 +121,7 @@ pub fn desugar_book(
   // Auto match linearization
   match opts.linearize_matches {
     OptLevel::Disabled => (),
-    OptLevel::Enabled => ctx.book.linearize_match_lambdas(),
+    OptLevel::Enabled => ctx.book.linearize_match_binds(),
     OptLevel::Extra => ctx.book.linearize_matches(),
   }
   // Manual match linearization
diff --git a/src/main.rs b/src/main.rs
index 8b6e86ce0..c29e97413 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -116,6 +116,9 @@ enum Mode {
     #[command(flatten)]
     transform_opts: TransformOpts,
 
+    #[arg(short = 'p', help = "Debug and normalization pretty printing")]
+    pretty: bool,
+
     #[arg(short = 'L', help = "Lazy mode")]
     lazy_mode: bool,
 
@@ -328,7 +331,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       println!("{}", compile_res.core_book);
     }
 
-    Mode::Desugar { path, comp_opts, warn_opts, lazy_mode, transform_opts } => {
+    Mode::Desugar { path, comp_opts, warn_opts, pretty, lazy_mode, transform_opts } => {
       let diagnostics_cfg = set_warning_cfg_from_cli(
         if lazy_mode { DiagnosticsConfig::default_lazy() } else { DiagnosticsConfig::default_strict() },
         lazy_mode,
@@ -341,7 +344,11 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       let diagnostics = desugar_book(&mut book, opts, diagnostics_cfg, None)?;
 
       eprint!("{diagnostics}");
-      println!("{book}");
+      if pretty {
+        println!("{}", book.display_pretty())
+      } else {
+        println!("{book}");
+      }
     }
 
     Mode::Run { lazy_mode, run_opts, pretty, comp_opts, transform_opts, warn_opts, arguments, path } => {
diff --git a/src/term/display.rs b/src/term/display.rs
index 21d73c91d..4169fcbaa 100644
--- a/src/term/display.rs
+++ b/src/term/display.rs
@@ -1,4 +1,4 @@
-use super::{Book, Definition, Name, NumCtr, Pattern, Rule, Tag, Term};
+use super::{Book, Definition, Name, Pattern, Rule, Tag, Term};
 use crate::maybe_grow;
 use std::{fmt, ops::Deref};
 
@@ -62,7 +62,7 @@ impl fmt::Display for Term {
       Term::App { tag, fun, arg } => {
         write!(f, "{}({} {})", tag.display_padded(), fun.display_app(tag), arg)
       }
-      Term::Mat { arg, with, rules } => {
+      Term::Mat { arg, bnd, with, arms: rules } => {
         let with: Box<dyn std::fmt::Display> = if with.is_empty() {
           Box::new(display!(""))
         } else {
@@ -70,25 +70,28 @@ impl fmt::Display for Term {
         };
         write!(
           f,
-          "match {}{} {{ {} }}",
+          "match {} = {}{} {{ {} }}",
+          bnd.as_ref().unwrap(),
           arg,
           with,
           DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", var_as_str(&rule.0), rule.2)), "; "),
         )
       }
-      Term::Swt { arg, with, rules } => {
+      Term::Swt { arg, bnd, with, pred: _, arms } => {
         let with: Box<dyn std::fmt::Display> = if with.is_empty() {
           Box::new(display!(""))
         } else {
           Box::new(display!(" with {}", DisplayJoin(|| with, ", ")))
         };
-        write!(
-          f,
-          "switch {}{} {{ {} }}",
-          arg,
-          with,
-          DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", rule.0, rule.1)), "; "),
-        )
+        let arms = DisplayJoin(
+          || {
+            arms.iter().enumerate().map(|(i, rule)| {
+              display!("{}: {}", if i == arms.len() - 1 { "_".to_string() } else { i.to_string() }, rule)
+            })
+          },
+          "; ",
+        );
+        write!(f, "switch {} = {}{} {{ {} }}", bnd.as_ref().unwrap(), arg, with, arms)
       }
       Term::Ltp { bnd, val, nxt } => {
         write!(f, "let ({}) = {}; {}", DisplayJoin(|| bnd.iter().map(var_as_str), ", "), val, nxt)
@@ -163,15 +166,6 @@ impl fmt::Display for Book {
   }
 }
 
-impl fmt::Display for NumCtr {
-  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-    match self {
-      NumCtr::Num(n) => write!(f, "{n}"),
-      NumCtr::Succ(_) => write!(f, "_"),
-    }
-  }
-}
-
 impl fmt::Display for Name {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     self.0.fmt(f)
@@ -180,11 +174,13 @@ impl fmt::Display for Name {
 
 impl Term {
   fn display_app<'a>(&'a self, tag: &'a Tag) -> impl fmt::Display + 'a {
-    DisplayFn(move |f| match self {
-      Term::App { tag: tag2, fun, arg } if tag2 == tag => {
-        write!(f, "{} {}", fun.display_app(tag), arg)
-      }
-      _ => write!(f, "{}", self),
+    maybe_grow(|| {
+      DisplayFn(move |f| match self {
+        Term::App { tag: tag2, fun, arg } if tag2 == tag => {
+          write!(f, "{} {}", fun.display_app(tag), arg)
+        }
+        _ => write!(f, "{}", self),
+      })
     })
   }
 }
@@ -204,6 +200,31 @@ fn var_as_str(nam: &Option<Name>) -> &str {
   nam.as_ref().map_or("*", Name::deref)
 }
 
+/* Pretty printing  */
+
+impl Book {
+  pub fn display_pretty(&self) -> impl fmt::Display + '_ {
+    display!("{}", DisplayJoin(|| self.defs.values().map(|def| def.display_pretty()), "\n\n"))
+  }
+}
+
+impl Definition {
+  pub fn display_pretty(&self) -> impl fmt::Display + '_ {
+    display!("{}", DisplayJoin(|| self.rules.iter().map(|x| x.display_pretty(&self.name)), "\n"))
+  }
+}
+
+impl Rule {
+  pub fn display_pretty<'a>(&'a self, def_name: &'a Name) -> impl fmt::Display + 'a {
+    display!(
+      "({}{}) =\n  {}",
+      def_name,
+      DisplayJoin(|| self.pats.iter().map(|x| display!(" {x}")), ""),
+      self.body.display_pretty(2)
+    )
+  }
+}
+
 impl Term {
   pub fn display_pretty(&self, tab: usize) -> impl fmt::Display + '_ {
     maybe_grow(|| {
@@ -221,23 +242,44 @@ impl Term {
         Term::Lnk { nam } => write!(f, "${nam}"),
 
         Term::Let { nam, val, nxt } => {
-          write!(f, "let {} = {};\n{}", var_as_str(nam), val.display_pretty(tab), nxt.display_pretty(tab))
+          write!(
+            f,
+            "let {} = {};\n{:tab$}{}",
+            var_as_str(nam),
+            val.display_pretty(tab),
+            "",
+            nxt.display_pretty(tab)
+          )
         }
 
         Term::Use { nam, val, nxt } => {
-          write!(f, "use {} = {};\n{}", var_as_str(nam), val.display_pretty(tab), nxt.display_pretty(tab))
+          write!(
+            f,
+            "use {} = {};\n{:tab$}{}",
+            var_as_str(nam),
+            val.display_pretty(tab),
+            "",
+            nxt.display_pretty(tab)
+          )
         }
 
         Term::App { tag, fun, arg } => {
-          write!(f, "{}({} {})", tag.display_padded(), fun.display_pretty(tab), arg.display_pretty(tab))
+          write!(
+            f,
+            "{}({} {})",
+            tag.display_padded(),
+            fun.display_app_pretty(tag, tab),
+            arg.display_pretty(tab)
+          )
         }
 
         Term::Ltp { bnd, val, nxt } => {
           write!(
             f,
-            "let ({}) = {};\n{}",
+            "let ({}) = {};\n{:tab$}{}",
             DisplayJoin(|| bnd.iter().map(var_as_str), ", "),
             val.display_pretty(tab),
+            "",
             nxt.display_pretty(tab),
           )
         }
@@ -249,10 +291,11 @@ impl Term {
         Term::Dup { tag, bnd, val, nxt } => {
           write!(
             f,
-            "let {}{{{}}} = {};\n{}",
+            "let {}{{{}}} = {};\n{:tab$}{}",
             tag.display_padded(),
             DisplayJoin(|| bnd.iter().map(var_as_str), " "),
             val.display_pretty(tab),
+            "",
             nxt.display_pretty(tab),
           )
         }
@@ -274,7 +317,7 @@ impl Term {
           write!(f, "({} {} {})", opr, fst.display_pretty(tab), snd.display_pretty(tab))
         }
 
-        Term::Mat { arg, with, rules } => {
+        Term::Mat { bnd, arg, with, arms } => {
           let with: Box<dyn std::fmt::Display> = if with.is_empty() {
             Box::new(DisplayFn(|f| write!(f, "")))
           } else {
@@ -282,14 +325,14 @@ impl Term {
               write!(f, "with {}", DisplayJoin(|| with.iter().map(|e| e.to_string()), ", "))
             }))
           };
-          writeln!(f, "match {} {}{{", arg.display_pretty(tab), with)?;
-          for rule in rules {
+          writeln!(f, "match {} = {} {}{{", var_as_str(bnd), arg.display_pretty(tab), with)?;
+          for rule in arms {
             writeln!(
               f,
-              "{:tab$}{}: {}",
+              "{:tab$}{}: {};",
               "",
               var_as_str(&rule.0),
-              rule.2.display_pretty(tab + 2),
+              rule.2.display_pretty(tab + 4),
               tab = tab + 2
             )?;
           }
@@ -297,17 +340,22 @@ impl Term {
           Ok(())
         }
 
-        Term::Swt { arg, with, rules } => {
+        Term::Swt { bnd, arg, with, pred: _, arms } => {
           let with: Box<dyn std::fmt::Display> = if with.is_empty() {
-            Box::new(DisplayFn(|f| write!(f, "")))
+            Box::new(display!(""))
           } else {
-            Box::new(DisplayFn(|f| {
-              write!(f, "with {}", DisplayJoin(|| with.iter().map(|e| e.to_string()), ", "))
-            }))
+            Box::new(display!(" with {}", DisplayJoin(|| with, ", ")))
           };
-          writeln!(f, "switch {} {}{{", arg.display_pretty(tab), with)?;
-          for rule in rules {
-            writeln!(f, "{:tab$}{}: {}", "", rule.0, rule.1.display_pretty(tab + 2), tab = tab + 2)?;
+          writeln!(f, "switch {} = {} {}{{", var_as_str(bnd), arg.display_pretty(tab), with)?;
+          for (i, rule) in arms.iter().enumerate() {
+            writeln!(
+              f,
+              "{:tab$}{}: {};",
+              "",
+              if i == arms.len() - 1 { "_".to_string() } else { i.to_string() },
+              rule.display_pretty(tab + 4),
+              tab = tab + 2
+            )?;
           }
           write!(f, "{:tab$}}}", "")?;
           Ok(())
@@ -322,4 +370,15 @@ impl Term {
       })
     })
   }
+
+  fn display_app_pretty<'a>(&'a self, tag: &'a Tag, tab: usize) -> impl fmt::Display + 'a {
+    maybe_grow(|| {
+      DisplayFn(move |f| match self {
+        Term::App { tag: tag2, fun, arg } if tag2 == tag => {
+          write!(f, "{} {}", fun.display_app_pretty(tag, tab), arg.display_pretty(tab))
+        }
+        _ => write!(f, "{}", self.display_pretty(tab)),
+      })
+    })
+  }
 }
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 5ae8e1b81..ca0a8cc1f 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -1,4 +1,3 @@
-use self::parser::STRINGS;
 use crate::{
   diagnostics::{Diagnostics, DiagnosticsConfig},
   maybe_grow,
@@ -6,7 +5,7 @@ use crate::{
   ENTRY_POINT,
 };
 use indexmap::{IndexMap, IndexSet};
-use interner::global::GlobalString;
+use interner::global::{GlobalPool, GlobalString};
 use itertools::Itertools;
 use std::{borrow::Cow, collections::HashMap, ops::Deref};
 
@@ -23,6 +22,7 @@ pub use hvmc::ops::{IntOp, Op, Ty as OpType};
 pub use net_to_term::{net_to_term, ReadbackError};
 pub use term_to_net::{book_to_nets, term_to_compat_net};
 
+pub static STRINGS: GlobalPool<String> = GlobalPool::new();
 #[derive(Debug)]
 pub struct Ctx<'book> {
   pub book: &'book mut Book,
@@ -144,14 +144,17 @@ pub enum Term {
   /// Pattern matching on an ADT.
   Mat {
     arg: Box<Term>,
+    bnd: Option<Name>,
     with: Vec<Name>,
-    rules: Vec<MatchRule>,
+    arms: Vec<MatchRule>,
   },
   /// Native pattern matching on numbers
   Swt {
     arg: Box<Term>,
+    bnd: Option<Name>,
     with: Vec<Name>,
-    rules: Vec<SwitchRule>,
+    pred: Option<Name>,
+    arms: Vec<Term>,
   },
   Ref {
     nam: Name,
@@ -162,7 +165,6 @@ pub enum Term {
 }
 
 pub type MatchRule = (Option<Name>, Vec<Option<Name>>, Term);
-pub type SwitchRule = (NumCtr, Term);
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Pattern {
@@ -174,17 +176,12 @@ pub enum Pattern {
   Str(GlobalString),
 }
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub enum NumCtr {
-  Num(u64),
-  Succ(Option<Name>),
-}
-
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
 pub enum Tag {
   Named(Name),
   Numeric(u32),
   Auto,
+  #[default]
   Static,
 }
 
@@ -323,12 +320,16 @@ impl Clone for Term {
       Self::Str { val } => Self::Str { val: val.clone() },
       Self::Lst { els } => Self::Lst { els: els.clone() },
       Self::Opx { opr, fst, snd } => Self::Opx { opr: *opr, fst: fst.clone(), snd: snd.clone() },
-      Self::Mat { arg, with, rules } => {
-        Self::Mat { arg: arg.clone(), with: with.clone(), rules: rules.clone() }
-      }
-      Self::Swt { arg, with, rules } => {
-        Self::Swt { arg: arg.clone(), with: with.clone(), rules: rules.clone() }
-      }
+      Self::Mat { arg, bnd, with, arms } => {
+        Self::Mat { arg: arg.clone(), bnd: bnd.clone(), with: with.clone(), arms: arms.clone() }
+      }
+      Self::Swt { arg, bnd, with, pred, arms } => Self::Swt {
+        arg: arg.clone(),
+        bnd: bnd.clone(),
+        with: with.clone(),
+        pred: pred.clone(),
+        arms: arms.clone(),
+      },
       Self::Ref { nam } => Self::Ref { nam: nam.clone() },
       Self::Era => Self::Era,
       Self::Err => Self::Err,
@@ -424,10 +425,9 @@ impl Term {
     Term::Str { val: STRINGS.get(str) }
   }
 
-  pub fn switch(arg: Term, zero: Term, succ: Term, succ_var: Option<Name>) -> Term {
-    let zero = (NumCtr::Num(0), zero);
-    let succ = (NumCtr::Succ(succ_var), succ);
-    Term::Swt { arg: Box::new(arg), with: vec![], rules: vec![zero, succ] }
+  pub fn switch(arg: Term, bnd: Name, zero: Term, succ: Term) -> Term {
+    let pred = Some(Name::new(format!("{bnd}-1")));
+    Term::Swt { arg: Box::new(arg), bnd: Some(bnd), with: vec![], pred, arms: vec![zero, succ] }
   }
 
   pub fn sub_num(arg: Term, val: u64) -> Term {
@@ -458,11 +458,11 @@ impl Term {
   pub fn children(&self) -> impl DoubleEndedIterator<Item = &Term> + Clone {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
     match self {
-      Term::Mat { arg, with: _, rules } => {
-        ChildrenIter::Mat([arg.as_ref()].into_iter().chain(rules.iter().map(|r| &r.2)))
+      Term::Mat { arg, bnd: _, with: _, arms } => {
+        ChildrenIter::Mat([arg.as_ref()].into_iter().chain(arms.iter().map(|r| &r.2)))
       }
-      Term::Swt { arg, with: _, rules } => {
-        ChildrenIter::Swt([arg.as_ref()].into_iter().chain(rules.iter().map(|r| &r.1)))
+      Term::Swt { arg, bnd: _, with: _, pred: _, arms } => {
+        ChildrenIter::Swt([arg.as_ref()].into_iter().chain(arms))
       }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => ChildrenIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
@@ -486,11 +486,11 @@ impl Term {
   pub fn children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
     match self {
-      Term::Mat { arg, with: _, rules } => {
+      Term::Mat { arg, bnd: _, with: _, arms: rules } => {
         ChildrenIter::Mat([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.2)))
       }
-      Term::Swt { arg, with: _, rules } => {
-        ChildrenIter::Swt([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.1)))
+      Term::Swt { arg, bnd: _, with: _, pred: _, arms } => {
+        ChildrenIter::Swt([arg.as_mut()].into_iter().chain(arms))
       }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => ChildrenIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
@@ -514,6 +514,8 @@ impl Term {
   /// An iterator over the subterms with an iterator over the binds
   /// introduced by the current term for each subterm.
   ///
+  /// Must only be called after fix_matches.
+  ///
   /// Example: A lambda introduces 1 bind for it's only subterm,
   /// while a let expression introduces 0 binds for the value and
   /// many binds for the next term.
@@ -522,20 +524,21 @@ impl Term {
   ) -> impl DoubleEndedIterator<Item = (&Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)> + Clone
   {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
-    multi_iterator!(BindsIter { Zero, One, Dup, Mat });
+    multi_iterator!(BindsIter { Zero, One, Two, Dup, Mat });
     match self {
-      Term::Mat { arg, with: _, rules } => ChildrenIter::Mat(
+      Term::Mat { arg, bnd, with: _, arms: rules } => ChildrenIter::Mat(
         [(arg.as_ref(), BindsIter::Zero([]))]
           .into_iter()
-          .chain(rules.iter().map(|r| (&r.2, BindsIter::Mat(r.1.iter())))),
+          .chain(rules.iter().map(move |r| (&r.2, BindsIter::Mat([bnd].into_iter().chain(r.1.iter()))))),
       ),
-      Term::Swt { arg, with: _, rules } => {
-        ChildrenIter::Swt([(arg.as_ref(), BindsIter::Zero([]))].into_iter().chain(rules.iter().map(|r| {
-          match &r.0 {
-            NumCtr::Num(_) => (&r.1, BindsIter::Zero([])),
-            NumCtr::Succ(nam) => (&r.1, BindsIter::One([nam])),
-          }
-        })))
+      Term::Swt { arg, bnd, with: _, pred, arms: rules } => {
+        let (succ, nums) = rules.split_last().unwrap();
+        ChildrenIter::Swt(
+          [(arg.as_ref(), BindsIter::Zero([]))]
+            .into_iter()
+            .chain(nums.iter().map(move |x| (x, BindsIter::One([bnd]))))
+            .chain([(succ, BindsIter::Two([bnd, pred]))]),
+        )
       }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => {
         ChildrenIter::Vec(els.iter().map(|el| (el, BindsIter::Zero([]))))
@@ -543,7 +546,9 @@ impl Term {
       Term::Let { nam, val, nxt, .. } => {
         ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::One([nam]))])
       }
-      Term::Use { .. } => todo!(),
+      Term::Use { nam, val, nxt, .. } => {
+        ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::One([nam]))])
+      }
       Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => {
         ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::Dup(bnd))])
       }
@@ -563,24 +568,30 @@ impl Term {
     }
   }
 
+  /// Must only be called after fix_matches.
   pub fn children_mut_with_binds(
     &mut self,
   ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)>
   {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
-    multi_iterator!(BindsIter { Zero, One, Dup, Mat });
+    multi_iterator!(BindsIter { Zero, One, Two, Dup, Mat });
     match self {
-      Term::Mat { arg, with: _, rules } => ChildrenIter::Mat(
-        [(arg.as_mut(), BindsIter::Zero([]))]
-          .into_iter()
-          .chain(rules.iter_mut().map(|r| (&mut r.2, BindsIter::Mat(r.1.iter())))),
-      ),
-      Term::Swt { arg, with: _, rules } => ChildrenIter::Swt(
-        [(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain(rules.iter_mut().map(|r| match &r.0 {
-          NumCtr::Num(_) => (&mut r.1, BindsIter::Zero([])),
-          NumCtr::Succ(nam) => (&mut r.1, BindsIter::One([nam])),
-        })),
-      ),
+      Term::Mat { arg, bnd, with: _, arms: rules } => {
+        let bnd = &*bnd;
+        ChildrenIter::Mat([(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain(
+          rules.iter_mut().map(move |r| (&mut r.2, BindsIter::Mat([bnd].into_iter().chain(r.1.iter())))),
+        ))
+      }
+      Term::Swt { arg, bnd, with: _, pred, arms: rules } => {
+        let bnd = &*bnd;
+        let (succ, nums) = rules.split_last_mut().unwrap();
+        ChildrenIter::Swt(
+          [(arg.as_mut(), BindsIter::Zero([]))]
+            .into_iter()
+            .chain(nums.iter_mut().map(move |x| (x, BindsIter::One([bnd]))))
+            .chain([(succ, BindsIter::Two([bnd, &*pred]))]),
+        )
+      }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => {
         ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
       }
@@ -609,23 +620,27 @@ impl Term {
     }
   }
 
+  /// Must only be called after fix_matches.
   pub fn children_mut_with_binds_mut(
     &mut self,
   ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &mut Option<Name>>)> {
     multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
     multi_iterator!(BindsIter { Zero, One, Dup, Mat });
     match self {
-      Term::Mat { arg, with: _, rules } => ChildrenIter::Mat(
+      Term::Mat { arg, bnd: _, with: _, arms: rules } => ChildrenIter::Mat(
         [(arg.as_mut(), BindsIter::Zero([]))]
           .into_iter()
           .chain(rules.iter_mut().map(|r| (&mut r.2, BindsIter::Mat(r.1.iter_mut())))),
       ),
-      Term::Swt { arg, with: _, rules } => ChildrenIter::Swt(
-        [(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain(rules.iter_mut().map(|r| match &mut r.0 {
-          NumCtr::Num(_) => (&mut r.1, BindsIter::Zero([])),
-          NumCtr::Succ(nam) => (&mut r.1, BindsIter::One([nam])),
-        })),
-      ),
+      Term::Swt { arg, bnd: _, with: _, pred, arms: rules } => {
+        let (succ, nums) = rules.split_last_mut().unwrap();
+        ChildrenIter::Swt(
+          [(arg.as_mut(), BindsIter::Zero([]))]
+            .into_iter()
+            .chain(nums.iter_mut().map(|x| (x, BindsIter::Zero([]))))
+            .chain([(succ, BindsIter::One([pred]))]),
+        )
+      }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => {
         ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
       }
diff --git a/src/term/net_to_term.rs b/src/term/net_to_term.rs
index e9662f457..98232d7ea 100644
--- a/src/term/net_to_term.rs
+++ b/src/term/net_to_term.rs
@@ -114,7 +114,7 @@ impl Reader<'_> {
             if *sel_kind != (Con { lab: None }) {
               // TODO: Is there any case where we expect a different node type here on readback?
               self.error(ReadbackError::InvalidNumericMatch);
-              Term::switch(arg, Term::Era, Term::Era, None)
+              Term::switch(arg, self.namegen.unique(), Term::Err, Term::Err)
             } else {
               let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
               let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
@@ -136,7 +136,7 @@ impl Reader<'_> {
                     bod.subst(nam, &Term::Var { nam: Name::new(format!("{arg}-1")) });
                   }
 
-                  let swt = Term::switch(Term::Var { nam: arg.clone() }, zero_term, *bod, nam);
+                  let swt = Term::switch(Term::Var { nam: arg.clone() }, arg.clone(), zero_term, *bod);
                   if let Some(bind) = bind {
                     Term::Let { nam: Some(arg), val: Box::new(bind), nxt: Box::new(swt) }
                   } else {
@@ -145,7 +145,7 @@ impl Reader<'_> {
                 }
                 _ => {
                   self.error(ReadbackError::InvalidNumericMatch);
-                  Term::switch(arg, zero_term, succ_term, None)
+                  Term::switch(arg, self.namegen.unique(), zero_term, succ_term)
                 }
               }
             }
diff --git a/src/term/parser.rs b/src/term/parser.rs
index ee11f43f2..18357b7c4 100644
--- a/src/term/parser.rs
+++ b/src/term/parser.rs
@@ -1,16 +1,13 @@
 use crate::{
   maybe_grow,
   term::{
-    display::DisplayFn, Adt, Book, Definition, IntOp, MatchRule, Name, NumCtr, Op, OpType, Pattern, Rule,
-    SwitchRule, Tag, Term,
+    display::DisplayFn, Adt, Book, Definition, IntOp, MatchRule, Name, Op, OpType, Pattern, Rule, Tag, Term,
+    STRINGS,
   },
 };
 use highlight_error::highlight_error;
-use interner::global::GlobalPool;
 use TSPL::Parser;
 
-pub static STRINGS: GlobalPool<String> = GlobalPool::new();
-
 // hvml grammar description:
 // <Book>       ::= (<Data> | <Rule>)*
 // <Data>       ::= "data" <Name> "=" ( <Name> | "(" <Name> (<Name>)* ")" )+
@@ -32,9 +29,9 @@ pub static STRINGS: GlobalPool<String> = GlobalPool::new();
 // <List>       ::= "[" (<Term> ","?)* "]"
 // <String>     ::= "\"" (escape sequence | [^"])* "\""
 // <Char>       ::= "'" (escape sequence | [^']) "'"
-// <Match>      ::= "match" (<Term> | <Name> "=" <Term>) ("with" <Var> (","? <Var>)*)? "{" <MatchArm>+ "}"
+// <Match>      ::= "match" <Name> ("=" <Term>)? ("with" <Var> (","? <Var>)*)? "{" <MatchArm>+ "}"
 // <MatchArm>   ::= "|"? <Pattern> ":" <Term> ";"?
-// <Switch>     ::= "match" (<Term> | <Name> "=" <Term>) ("with" <Var> (","? <Var>)*)? "{" <SwitchArm>+ "}"
+// <Switch>     ::= "switch" <Name> ("=" <Term>)? ("with" <Var> (","? <Var>)*)? "{" <SwitchArm>+ "}"
 // <SwitchArm>  ::= "|"? (<Num>|"_") ":" <Term> ";"?
 // <Var>        ::= <Name>
 // <UnscopedVar>::= "$" <Name>
@@ -172,7 +169,7 @@ impl<'a> TermParser<'a> {
           Pattern::Num(char as u64)
         }
         // Number
-        c if c.is_numeric() => {
+        c if c.is_ascii_digit() => {
           let num = self.parse_u64()?;
           Pattern::Num(num)
         }
@@ -261,7 +258,7 @@ impl<'a> TermParser<'a> {
         '#' => {
           let Some(head) = self.peek_many(2) else { return self.expected("tagged term or nat") };
           let head = head.chars().collect::<Vec<_>>();
-          if head[1].is_numeric() {
+          if head[1].is_ascii_digit() {
             // Nat
             self.consume("#")?;
             let val = self.parse_u64()?;
@@ -301,7 +298,7 @@ impl<'a> TermParser<'a> {
           Term::Num { val: chr as u64 }
         }
         // Native num
-        c if c.is_numeric() => {
+        c if c.is_ascii_digit() => {
           let val = self.parse_u64()?;
           Term::Num { val }
         }
@@ -358,79 +355,12 @@ impl<'a> TermParser<'a> {
             }
           } else if self.try_consume("match") {
             // match
-            let arg_ini_idx = *self.index();
-            let mut arg = self.parse_term()?;
-            let arg_end_idx = *self.index();
-
-            let (bnd, arg) = if self.skip_starts_with("=") {
-              if let Term::Var { nam } = &mut arg {
-                self.consume("=")?;
-                let term = self.parse_term()?;
-                (Some(std::mem::take(nam)), term)
-              } else {
-                return self.expected_spanned("var", arg_ini_idx, arg_end_idx);
-              }
-            } else {
-              (None, arg)
-            };
-            let with = if self.try_consume("with") {
-              let mut with = vec![self.parse_hvml_name()?];
-              while !self.skip_starts_with("{") {
-                self.try_consume(",");
-                with.push(self.parse_hvml_name()?);
-              }
-              with
-            } else {
-              vec![]
-            };
+            let (bnd, arg, with) = self.parse_match_arg()?;
             let rules = self.list_like(|p| p.parse_match_arm(), "{", "}", ";", false, 1)?;
-            if let Some(bnd) = bnd {
-              Term::Let {
-                nam: Some(bnd.clone()),
-                val: Box::new(arg),
-                nxt: Box::new(Term::Mat { arg: Box::new(Term::Var { nam: bnd }), with, rules }),
-              }
-            } else {
-              Term::Mat { arg: Box::new(arg), with, rules }
-            }
+            Term::Mat { arg: Box::new(arg), bnd: Some(bnd), with, arms: rules }
           } else if self.try_consume("switch") {
             // switch
-            let arg_ini_idx = *self.index();
-            let mut arg = self.parse_term()?;
-            let arg_end_idx = *self.index();
-
-            let (bnd, arg) = if self.skip_starts_with("=") {
-              if let Term::Var { nam } = &mut arg {
-                self.consume("=")?;
-                let term = self.parse_term()?;
-                (Some(std::mem::take(nam)), term)
-              } else {
-                return self.expected_spanned("var", arg_ini_idx, arg_end_idx);
-              }
-            } else {
-              (None, arg)
-            };
-            let with = if self.try_consume("with") {
-              let mut with = vec![self.parse_hvml_name()?];
-              while !self.skip_starts_with("{") {
-                self.try_consume(",");
-                with.push(self.parse_hvml_name()?);
-              }
-              with
-            } else {
-              vec![]
-            };
-            // TODO: we could enforce correct switches at the parser level to get a spanned error.
-            let rules = self.list_like(|p| p.parse_switch_arm(), "{", "}", ";", false, 1)?;
-            if let Some(bnd) = bnd {
-              Term::Let {
-                nam: Some(bnd.clone()),
-                val: Box::new(arg),
-                nxt: Box::new(Term::Swt { arg: Box::new(Term::Var { nam: bnd }), with, rules }),
-              }
-            } else {
-              Term::Swt { arg: Box::new(arg), with, rules }
-            }
+            self.parse_switch()?
           } else {
             // var
             let nam = self.labelled(|p| p.parse_hvml_name(), "term")?;
@@ -522,6 +452,22 @@ impl<'a> TermParser<'a> {
     Ok(Tag::Named(nam))
   }
 
+  fn parse_match_arg(&mut self) -> Result<(Name, Term, Vec<Name>), String> {
+    let bnd = self.parse_hvml_name()?;
+    let arg = if self.try_consume("=") { self.parse_term()? } else { Term::Var { nam: bnd.clone() } };
+    let with = if self.try_consume("with") {
+      let mut with = vec![self.parse_hvml_name()?];
+      while !self.skip_starts_with("{") {
+        self.try_consume(",");
+        with.push(self.parse_hvml_name()?);
+      }
+      with
+    } else {
+      vec![]
+    };
+    Ok((bnd, arg, with))
+  }
+
   fn parse_match_arm(&mut self) -> Result<MatchRule, String> {
     self.try_consume("|");
     let nam = self.parse_name_or_era()?;
@@ -530,23 +476,40 @@ impl<'a> TermParser<'a> {
     Ok((nam, vec![], bod))
   }
 
-  fn parse_switch_arm(&mut self) -> Result<SwitchRule, String> {
-    self.try_consume("|");
-    let Some(head) = self.skip_peek_one() else { return self.expected("switch pattern") };
-    let ctr = match head {
-      '_' => {
-        self.consume("_")?;
-        NumCtr::Succ(None)
-      }
-      c if c.is_numeric() => {
-        let val = self.parse_u64()?;
-        NumCtr::Num(val)
-      }
-      _ => return self.expected("switch pattern"),
-    };
-    self.consume(":")?;
-    let bod = self.parse_term()?;
-    Ok((ctr, bod))
+  fn parse_switch(&mut self) -> Result<Term, String> {
+    let (bnd, arg, with) = self.parse_match_arg()?;
+    self.consume("{")?;
+    let mut expected_num = 0;
+    let mut arms = vec![];
+    let mut to_continue = true;
+    while to_continue && !self.skip_starts_with("}") {
+      self.try_consume("|");
+      let Some(head) = self.skip_peek_one() else { return self.expected("switch pattern") };
+      match head {
+        '_' => {
+          if expected_num == 0 {
+            return self.expected("0");
+          } else {
+            self.consume("_")?;
+            to_continue = false;
+          }
+        }
+        c if c.is_ascii_digit() => {
+          let val = self.parse_u64()?;
+          if val != expected_num {
+            return self.expected(&expected_num.to_string());
+          }
+        }
+        _ => return self.expected("switch pattern"),
+      };
+      self.consume(":")?;
+      arms.push(self.parse_term()?);
+      self.try_consume(";");
+      expected_num += 1;
+    }
+    let pred = Some(Name::new(format!("{}-{}", bnd, arms.len() - 1)));
+    self.consume("}")?;
+    Ok(Term::Swt { arg: Box::new(arg), bnd: Some(bnd), with, pred, arms })
   }
 
   /* Utils */
diff --git a/src/term/term_to_net.rs b/src/term/term_to_net.rs
index e98026893..31bd33db9 100644
--- a/src/term/term_to_net.rs
+++ b/src/term/term_to_net.rs
@@ -5,7 +5,7 @@ use crate::{
     NodeKind::{self, *},
     Port, ROOT,
   },
-  term::{Book, Name, NumCtr, Tag, Term},
+  term::{Book, Name, Tag, Term},
 };
 use std::collections::{hash_map::Entry, HashMap};
 
@@ -43,8 +43,8 @@ pub fn term_to_compat_net(term: &Term, labels: &mut Labels) -> INet {
 
   let main = state.encode_term(term, ROOT);
 
-  for (decl_port, use_port) in std::mem::take(&mut state.global_vars).into_values() {
-    state.inet.link(decl_port, use_port);
+  for (decl_port, use_port) in state.global_vars.values() {
+    state.inet.link(*decl_port, *use_port);
   }
   if Some(ROOT) != main {
     state.link_local(ROOT, main);
@@ -114,20 +114,18 @@ impl EncodeTermState<'_> {
         }
         Term::Mat { .. } => unreachable!("Should've been desugared already"),
         // core: & arg ~ ?<(zero succ) ret>
-        Term::Swt { arg, with, rules } => {
+        Term::Swt { arg, bnd: _, with, pred: _, arms: rules } => {
           // At this point should be only num matches of 0 and succ.
           assert!(with.is_empty());
           assert!(rules.len() == 2);
-          assert!(matches!(rules[0].0, NumCtr::Num(0)));
-          assert!(matches!(rules[1].0, NumCtr::Succ(None)));
 
           let mat = self.inet.new_node(Mat);
 
           let arg = self.encode_term(arg, Port(mat, 0));
           self.link_local(Port(mat, 0), arg);
 
-          let zero = &rules[0].1;
-          let succ = &rules[1].1;
+          let zero = &rules[0];
+          let succ = &rules[1];
 
           let sel = self.inet.new_node(Con { lab: None });
           self.inet.link(Port(sel, 0), Port(mat, 1));
diff --git a/src/term/transform/desugar_match_defs.rs b/src/term/transform/desugar_match_defs.rs
index 41c5b0fa7..cc4cd7f04 100644
--- a/src/term/transform/desugar_match_defs.rs
+++ b/src/term/transform/desugar_match_defs.rs
@@ -1,6 +1,6 @@
 use crate::{
   diagnostics::{Diagnostics, ToStringVerbose, WarningType},
-  term::{builtins, Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term},
+  term::{builtins, Adts, Constructors, Ctx, Definition, Name, Pattern, Rule, Term},
 };
 use std::collections::{BTreeSet, HashSet};
 
@@ -99,15 +99,15 @@ fn fix_repeated_binds(rules: &mut [Rule]) -> Vec<DesugarMatchDefErr> {
 /// Linearizes all the arguments that are used in at least one of the bodies.
 fn simplify_rule_match(
   args: Vec<Name>,
-  mut rules: Vec<Rule>,
+  rules: Vec<Rule>,
   with: Vec<Name>,
   ctrs: &Constructors,
   adts: &Adts,
 ) -> Result<Term, DesugarMatchDefErr> {
   if args.is_empty() {
-    Ok(std::mem::take(&mut rules[0].body))
+    Ok(rules.into_iter().next().unwrap().body)
   } else if rules[0].pats.iter().all(|p| p.is_wildcard()) {
-    Ok(irrefutable_fst_row_rule(args, std::mem::take(&mut rules[0])))
+    Ok(irrefutable_fst_row_rule(args, rules.into_iter().next().unwrap()))
   } else {
     let typ = Type::infer_from_def_arg(&rules, 0, ctrs)?;
     match typ {
@@ -239,8 +239,7 @@ fn num_rule(
   let arg = args[0].clone();
   let args = args.split_off(1);
 
-  let match_var = Name::new(format!("{arg}%matched"));
-  let pred_var = Name::new(format!("{arg}%matched-1"));
+  let pred_var = Name::new(format!("{arg}-1"));
 
   // Since numbers have infinite (2^60) constructors, they require special treatment.
   // We first iterate over each present number then get the default.
@@ -299,32 +298,21 @@ fn num_rule(
   let swt_with = with.into_iter().chain(args).collect::<Vec<_>>();
 
   let term = num_bodies.into_iter().enumerate().rfold(default_body, |term, (i, body)| {
-    let zero = (NumCtr::Num(0), body);
-    let succ = (NumCtr::Succ(Some(pred_var.clone())), term);
-    let mut swt = Term::Swt {
-      arg: Box::new(Term::Var { nam: match_var.clone() }),
-      with: swt_with.clone(),
-      rules: vec![zero, succ],
-    };
-
     let val = if i > 0 {
-      // let %matched = (%matched-1 +1 +num_i-1 - num_i)
-      //  switch %matched { 0: body_i; _: acc }
+      //  switch arg = (pred +1 +num_i-1 - num_i) { 0: body_i; _: acc }
       // nums[i] >= nums[i-1]+1, so we do a sub here.
       Term::sub_num(Term::Var { nam: pred_var.clone() }, nums[i] - 1 - nums[i - 1])
     } else {
-      // let %matched = (arg -num_0);
-      //  switch %matched { 0: body_0; _: acc}
+      //  switch arg = (arg -num_0) { 0: body_0; _: acc}
       Term::sub_num(Term::Var { nam: arg.clone() }, nums[i])
     };
 
-    if let Term::Var { .. } = &val {
-      // No need to create a let expression if it's just a rename.
-      // We know that the bound value is a uniquely named var, so we can subst.
-      swt.subst(&match_var, &val);
-      swt
-    } else {
-      Term::Let { nam: Some(match_var.clone()), val: Box::new(val), nxt: Box::new(swt) }
+    Term::Swt {
+      arg: Box::new(val),
+      bnd: Some(arg.clone()),
+      with: swt_with.clone(),
+      pred: Some(pred_var.clone()),
+      arms: vec![body, term],
     }
   });
 
@@ -443,7 +431,12 @@ fn switch_rule(
   // Linearize previously matched vars and current args.
   let mat_with = with.into_iter().chain(old_args).collect::<Vec<_>>();
 
-  let term = Term::Mat { arg: Box::new(Term::Var { nam: arg }), with: mat_with, rules: new_arms };
+  let term = Term::Mat {
+    arg: Box::new(Term::Var { nam: arg.clone() }),
+    bnd: Some(arg.clone()),
+    with: mat_with,
+    arms: new_arms,
+  };
   Ok(term)
 }
 
diff --git a/src/term/transform/encode_match_terms.rs b/src/term/transform/encode_match_terms.rs
index 0d5ddc6a0..2950cb8fb 100644
--- a/src/term/transform/encode_match_terms.rs
+++ b/src/term/transform/encode_match_terms.rs
@@ -1,6 +1,6 @@
 use crate::{
   maybe_grow,
-  term::{AdtEncoding, Book, Constructors, MatchRule, Name, NumCtr, SwitchRule, Tag, Term},
+  term::{AdtEncoding, Adts, Book, Constructors, MatchRule, Name, Tag, Term},
 };
 
 impl Book {
@@ -15,36 +15,55 @@ impl Book {
   pub fn encode_matches(&mut self, adt_encoding: AdtEncoding) {
     for def in self.defs.values_mut() {
       for rule in &mut def.rules {
-        rule.body.encode_matches(&self.ctrs, adt_encoding);
+        rule.body.encode_matches(&self.ctrs, &self.adts, adt_encoding);
       }
     }
   }
 }
 
 impl Term {
-  pub fn encode_matches(&mut self, ctrs: &Constructors, adt_encoding: AdtEncoding) {
+  pub fn encode_matches(&mut self, ctrs: &Constructors, adts: &Adts, adt_encoding: AdtEncoding) {
     maybe_grow(|| {
       for child in self.children_mut() {
-        child.encode_matches(ctrs, adt_encoding)
+        child.encode_matches(ctrs, adts, adt_encoding)
       }
 
-      if let Term::Mat { arg, with, rules } = self {
+      if let Term::Mat { arg, bnd, with, arms: rules } = self {
         assert!(with.is_empty());
+        let bnd = std::mem::take(bnd).unwrap();
         let arg = std::mem::take(arg.as_mut());
         let rules = std::mem::take(rules);
-        *self = encode_match(arg, rules, ctrs, adt_encoding);
-      } else if let Term::Swt { arg, with, rules } = self {
+        *self = encode_match(bnd, arg, rules, ctrs, adts, adt_encoding);
+      } else if let Term::Swt { arg, bnd, with, pred, arms: rules } = self {
         assert!(with.is_empty());
+        let bnd = std::mem::take(bnd).unwrap();
         let arg = std::mem::take(arg.as_mut());
+        let pred = std::mem::take(pred);
         let rules = std::mem::take(rules);
-        *self = encode_switch(arg, rules);
+        *self = encode_switch(bnd, arg, pred, rules);
       }
     })
   }
 }
 
-fn encode_match(arg: Term, rules: Vec<MatchRule>, ctrs: &Constructors, adt_encoding: AdtEncoding) -> Term {
-  let adt = ctrs.get(rules[0].0.as_ref().unwrap()).unwrap();
+fn encode_match(
+  bnd: Name,
+  arg: Term,
+  mut rules: Vec<MatchRule>,
+  ctrs: &Constructors,
+  adts: &Adts,
+  adt_encoding: AdtEncoding,
+) -> Term {
+  let adt_nam = ctrs.get(rules[0].0.as_ref().unwrap()).unwrap();
+
+  // Add a `use` term reconstructing the matched variable to each arm.
+  for rule in rules.iter_mut() {
+    let ctr = rule.0.clone().unwrap();
+    let fields = adts[adt_nam].ctrs[&ctr].iter().map(|f| Term::Var { nam: Name::new(format!("{bnd}.{f}")) });
+    let orig = Term::call(Term::Ref { nam: ctr }, fields);
+    rule.2 =
+      Term::Use { nam: Some(bnd.clone()), val: Box::new(orig), nxt: Box::new(std::mem::take(&mut rule.2)) };
+  }
 
   // ADT Encoding depends on compiler option
   match adt_encoding {
@@ -62,96 +81,46 @@ fn encode_match(arg: Term, rules: Vec<MatchRule>, ctrs: &Constructors, adt_encod
       let mut arms = vec![];
       for rule in rules.into_iter() {
         let body =
-          rule.1.iter().cloned().rfold(rule.2, |bod, nam| Term::tagged_lam(Tag::adt_name(adt), nam, bod));
+          rule.1.iter().cloned().rfold(rule.2, |bod, nam| Term::tagged_lam(Tag::adt_name(adt_nam), nam, bod));
         arms.push(body);
       }
-      Term::tagged_call(Tag::adt_name(adt), arg, arms)
+      Term::tagged_call(Tag::adt_name(adt_nam), arg, arms)
     }
   }
 }
 
-/// Convert into a sequence of native matches, decrementing by 1 each match.
-/// match n {0: A; 1: B; 2+: (C n-2)} converted to
-/// match n {0: A; 1+: @%x match %x {0: B; 1+: @n-2 (C n-2)}}
-fn encode_switch(arg: Term, mut rules: Vec<SwitchRule>) -> Term {
-  let last_rule = rules.pop().unwrap();
+/// Convert into a sequence of native switches, decrementing by 1 each switch.
+/// switch n {0: A; 1: B; _: (C n-2)} converted to
+/// switch n {0: A; _: @%x match %x {0: B; _: @n-2 (C n-2)}}
+fn encode_switch(bnd: Name, arg: Term, pred: Option<Name>, mut rules: Vec<Term>) -> Term {
+  // Add a `use` term reconstructing the matched variable to each arm.
+  let n_nums = rules.len() - 1;
+  for (i, rule) in rules.iter_mut().enumerate() {
+    let orig = if i != n_nums {
+      Term::Num { val: i as u64 }
+    } else {
+      Term::add_num(Term::Var { nam: pred.clone().unwrap() }, n_nums as u64)
+    };
+    *rule = Term::Use { nam: Some(bnd.clone()), val: Box::new(orig), nxt: Box::new(std::mem::take(rule)) };
+  }
 
+  // Create the cascade of switches
   let match_var = Name::new("%x");
-
-  // @n-2 (C n-2)
-  let NumCtr::Succ(last_var) = last_rule.0 else { unreachable!() };
-  let last_arm = Term::lam(last_var, last_rule.1);
-
-  rules.into_iter().rfold(last_arm, |term, rule| {
-    let zero = (NumCtr::Num(0), rule.1);
-    let one = (NumCtr::Succ(None), term);
-    let rules = vec![zero, one];
-
-    let NumCtr::Num(num) = rule.0 else { unreachable!() };
-    if num == 0 {
-      Term::Swt { arg: Box::new(arg.clone()), with: vec![], rules }
+  let (succ, nums) = rules.split_last_mut().unwrap();
+  let last_arm = Term::lam(pred, std::mem::take(succ));
+  nums.iter_mut().enumerate().rfold(last_arm, |term, (i, rule)| {
+    let arms = vec![std::mem::take(rule), term];
+    if i == 0 {
+      Term::Swt { arg: Box::new(arg.clone()), bnd: Some(bnd.clone()), with: vec![], pred: None, arms }
     } else {
-      let swt = Term::Swt { arg: Box::new(Term::Var { nam: match_var.clone() }), with: vec![], rules };
+      let swt = Term::Swt {
+        arg: Box::new(Term::Var { nam: match_var.clone() }),
+        bnd: Some(match_var.clone()),
+        with: vec![],
+        pred: None,
+        arms,
+      };
       Term::named_lam(match_var.clone(), swt)
     }
   })
 }
-
-/* /// Convert into a sequence of native matches on (- n num_case)
-/// match n {a: A; b: B; n: (C n)} converted to
-/// match (- n a) {0: A; 1+: @%p match (- %p b-a-1) { 0: B; 1+: @%p let n = (+ %p b+1); (C n)}}
-fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
-  fn go(
-    mut rules: impl Iterator<Item = Rule>,
-    last_rule: Rule,
-    prev_num: Option<u64>,
-    arg: Option<Term>,
-  ) -> Term {
-    let rule = rules.next();
-    match (prev_num, rule) {
-      // Num matches must have at least 2 rules (1 num and 1 var).
-      // The first rule can't also be the last.
-      (None, None) => unreachable!(),
-      // First match
-      // match (- n a) {0: A; 1+: ...}
-      (None, Some(rule)) => {
-        let Pattern::Num(NumCtr::Num(val)) = &rule.pats[0] else { unreachable!() };
-        Term::switch(
-          Term::sub_num(arg.unwrap(), *val),
-          rule.body,
-          go(rules, last_rule, Some(*val), None),
-          None,
-        )
-      }
-      // Middle match
-      // @%p match (- %p b-a-1) { 0: B; 1+: ... }
-      (Some(prev_num), Some(rule)) => {
-        let Pattern::Num(NumCtr::Num(val)) = &rule.pats[0] else { unreachable!() };
-        let pred_nam = Name::from("%p");
-        Term::named_lam(
-          pred_nam.clone(),
-          Term::switch(
-            Term::sub_num(Term::Var { nam: pred_nam }, val.wrapping_sub(prev_num).wrapping_sub(1)),
-            rule.body,
-            go(rules, last_rule, Some(*val), None),
-            None,
-          ),
-        )
-      }
-      // Last match
-      // @%p let n = (+ %p b+1); (C n)
-      (Some(prev_num), None) => {
-        let pred_nam = Name::from("%p");
-        Term::named_lam(pred_nam.clone(), Term::Let {
-          pat: last_rule.pats.into_iter().next().unwrap(),
-          val: Box::new(Term::add_num(Term::Var { nam: pred_nam }, prev_num.wrapping_add(1))),
-          nxt: Box::new(last_rule.body),
-        })
-      }
-    }
-  }
-
-  let last_rule = rules.pop().unwrap();
-  go(rules.into_iter(), last_rule, None, Some(arg))
-}
- */
diff --git a/src/term/transform/fix_match_terms.rs b/src/term/transform/fix_match_terms.rs
index 788df4dee..74be11380 100644
--- a/src/term/transform/fix_match_terms.rs
+++ b/src/term/transform/fix_match_terms.rs
@@ -1,17 +1,15 @@
 use crate::{
   diagnostics::{Diagnostics, ToStringVerbose, WarningType},
   maybe_grow,
-  term::{Adts, Constructors, Ctx, MatchRule, Name, NumCtr, Term},
+  term::{Adts, Constructors, Ctx, MatchRule, Name, Term},
 };
 use std::collections::HashMap;
 
 enum FixMatchErr {
   AdtMismatch { expected: Name, found: Name, ctr: Name },
   NonExhaustiveMatch { typ: Name, missing: Name },
-  NumMismatch { expected: NumCtr, found: NumCtr },
   IrrefutableMatch { var: Option<Name> },
   UnreachableMatchArms { var: Option<Name> },
-  ExtraSwitchArms,
   RedundantArm { ctr: Name },
 }
 
@@ -52,11 +50,9 @@ impl Ctx<'_> {
 
         for err in errs {
           match err {
-            FixMatchErr::ExtraSwitchArms { .. }
-            | FixMatchErr::AdtMismatch { .. }
-            | FixMatchErr::NumMismatch { .. }
-            | FixMatchErr::NonExhaustiveMatch { .. } => self.info.add_rule_error(err, def.name.clone()),
-
+            FixMatchErr::AdtMismatch { .. } | FixMatchErr::NonExhaustiveMatch { .. } => {
+              self.info.add_rule_error(err, def.name.clone())
+            }
             FixMatchErr::IrrefutableMatch { .. } => {
               self.info.add_rule_warning(err, WarningType::IrrefutableMatch, def.name.clone())
             }
@@ -87,8 +83,6 @@ impl Term {
 
       if let Term::Mat { .. } = self {
         self.fix_match(&mut errs, ctrs, adts);
-      } else if let Term::Swt { .. } = self {
-        self.fix_switch(&mut errs);
       }
 
       errs
@@ -96,9 +90,8 @@ impl Term {
   }
 
   fn fix_match(&mut self, errs: &mut Vec<FixMatchErr>, ctrs: &Constructors, adts: &Adts) {
-    let Term::Mat { arg, with: _, rules } = self else { unreachable!() };
-
-    let (arg_nam, arg) = extract_match_arg(arg);
+    let Term::Mat { arg: _, bnd, with: _, arms: rules } = self else { unreachable!() };
+    let bnd = bnd.clone().unwrap();
 
     // Normalize arms, making one arm for each constructor of the matched adt.
     if let Some(ctr_nam) = &rules[0].0
@@ -107,12 +100,12 @@ impl Term {
       let adt_ctrs = &adts[adt_nam].ctrs;
 
       // Decide which constructor corresponds to which arm of the match.
-      let mut bodies = fixed_match_arms(rules, &arg_nam, adt_nam, adt_ctrs.keys(), ctrs, adts, errs);
+      let mut bodies = fixed_match_arms(&bnd, rules, adt_nam, adt_ctrs.keys(), ctrs, adts, errs);
 
       // Build the match arms, with all constructors
       let mut new_rules = vec![];
       for (ctr, fields) in adt_ctrs.iter() {
-        let fields = fields.iter().map(|f| Some(match_field(&arg_nam, f))).collect::<Vec<_>>();
+        let fields = fields.iter().map(|f| Some(match_field(&bnd, f))).collect::<Vec<_>>();
         let body = if let Some(Some(body)) = bodies.remove(ctr) {
           body
         } else {
@@ -125,75 +118,12 @@ impl Term {
     } else {
       // First arm was not matching a constructor, convert into a use term.
       errs.push(FixMatchErr::IrrefutableMatch { var: rules[0].0.clone() });
-
       let match_var = rules[0].0.take();
       *self = std::mem::take(&mut rules[0].2);
       if let Some(var) = match_var {
-        self.subst(&var, &Term::Var { nam: arg_nam.clone() });
-      }
-    }
-
-    *self = apply_arg(std::mem::take(self), arg_nam, arg);
-  }
-
-  /// For switches, the only necessary change is to add the implicit pred bind to the AST.
-  ///
-  /// Check that all numbers are in order and no cases are skipped.
-  /// Also check that we have a default case at the end, binding the pred.
-  fn fix_switch(&mut self, errs: &mut Vec<FixMatchErr>) {
-    let Term::Swt { arg, with: _, rules } = self else { unreachable!() };
-
-    let (arg_nam, arg) = extract_match_arg(arg);
-
-    let mut has_num = false;
-    let len = rules.len();
-    for i in 0 .. len {
-      let ctr = &mut rules[i].0;
-      match ctr {
-        NumCtr::Num(n) if i as u64 == *n => {
-          has_num = true;
-        }
-        NumCtr::Num(n) => {
-          errs.push(FixMatchErr::NumMismatch { expected: NumCtr::Num(i as u64), found: NumCtr::Num(*n) });
-          break;
-        }
-        NumCtr::Succ(pred) => {
-          if !has_num {
-            errs.push(FixMatchErr::NumMismatch {
-              expected: NumCtr::Num(i as u64),
-              found: NumCtr::Succ(pred.clone()),
-            });
-            break;
-          }
-          *pred = Some(Name::new(format!("{arg_nam}-{i}")));
-          if i != len - 1 {
-            errs.push(FixMatchErr::ExtraSwitchArms);
-            rules.truncate(i + 1);
-            break;
-          }
-        }
+        self.subst(&var, &Term::Var { nam: bnd.clone() });
       }
     }
-
-    *self = apply_arg(std::mem::take(self), arg_nam, arg);
-  }
-}
-
-fn extract_match_arg(arg: &mut Term) -> (Name, Option<Term>) {
-  if let Term::Var { nam } = arg {
-    (nam.clone(), None)
-  } else {
-    let nam = Name::new("%matched");
-    let arg = std::mem::replace(arg, Term::Var { nam: nam.clone() });
-    (nam, Some(arg))
-  }
-}
-
-fn apply_arg(term: Term, arg_nam: Name, arg: Option<Term>) -> Term {
-  if let Some(arg) = arg {
-    Term::Let { nam: Some(arg_nam), val: Box::new(arg), nxt: Box::new(term) }
-  } else {
-    term
   }
 }
 
@@ -203,8 +133,8 @@ fn apply_arg(term: Term, arg_nam: Name, arg: Option<Term>) -> Term {
 /// If no rules match a certain constructor, return None in the map,
 /// indicating a non-exhaustive match.
 fn fixed_match_arms<'a>(
+  bnd: &Name,
   rules: &mut Vec<MatchRule>,
-  arg_nam: &Name,
   adt_nam: &Name,
   adt_ctrs: impl Iterator<Item = &'a Name>,
   ctrs: &Constructors,
@@ -238,7 +168,7 @@ fn fixed_match_arms<'a>(
         if body.is_none() {
           let mut new_body = rules[rule_idx].2.clone();
           if let Some(var) = &rules[rule_idx].0 {
-            new_body.subst(var, &rebuild_ctr(arg_nam, ctr, &adts[adt_nam].ctrs[&**ctr]));
+            new_body.subst(var, &rebuild_ctr(bnd, ctr, &adts[adt_nam].ctrs[&**ctr]));
           }
           *body = Some(new_body);
         }
@@ -273,11 +203,6 @@ impl ToStringVerbose for FixMatchErr {
       FixMatchErr::NonExhaustiveMatch { typ, missing } => {
         format!("Non-exhaustive 'match' expression of type '{typ}'. Case '{missing}' not covered.")
       }
-      FixMatchErr::NumMismatch { expected, found } => {
-        format!(
-          "Malformed 'switch' expression. Expected case '{expected}', found '{found}'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case."
-        )
-      }
       FixMatchErr::IrrefutableMatch { var } => format!(
         "Irrefutable 'match' expression. All cases after '{}' will be ignored. If this is not a mistake, consider using a 'let' expression instead.",
         var.as_ref().unwrap_or(&Name::new("*"))
@@ -286,9 +211,6 @@ impl ToStringVerbose for FixMatchErr {
         "Unreachable arms in 'match' expression. All cases after '{}' will be ignored.",
         var.as_ref().unwrap_or(&Name::new("*"))
       ),
-      FixMatchErr::ExtraSwitchArms => {
-        "Extra arms in 'switch' expression. No rules should come after the default.".to_string()
-      }
       FixMatchErr::RedundantArm { ctr } => {
         format!("Redundant arm in 'match' expression. Case '{ctr}' appears more than once.")
       }
diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 06848aa73..9e135c09e 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -153,11 +153,11 @@ impl Term {
         args.push(app);
         FloatIter::App(args)
       }
-      Term::Mat { arg, with: _, rules } => {
-        FloatIter::Mat([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.2)))
+      Term::Mat { arg, bnd: _, with: _, arms } => {
+        FloatIter::Mat([arg.as_mut()].into_iter().chain(arms.iter_mut().map(|r| &mut r.2)))
       }
-      Term::Swt { arg, with: _, rules } => {
-        FloatIter::Swt([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.1)))
+      Term::Swt { arg, bnd: _, with: _, pred: _, arms } => {
+        FloatIter::Swt([arg.as_mut()].into_iter().chain(arms.iter_mut()))
       }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => FloatIter::Vec(els),
       Term::Ltp { val: fst, nxt: snd, .. }
diff --git a/src/term/transform/linearize_matches.rs b/src/term/transform/linearize_matches.rs
index 97af207e8..f2795b468 100644
--- a/src/term/transform/linearize_matches.rs
+++ b/src/term/transform/linearize_matches.rs
@@ -1,146 +1,201 @@
 use crate::{
   maybe_grow,
-  term::{Book, Name, NumCtr, Tag, Term},
+  term::{Book, Name, Term},
 };
 use std::collections::{BTreeSet, HashSet};
 
+/* Linearize preceding binds */
+
 impl Book {
-  /// Linearization of only eta-reducible match variables.
+  /// Linearization of binds preceding match/switch terms, up to the
+  /// first bind used in either the scrutinee or the bind.
   ///
   /// Example:
   /// ```hvm
-  /// @a @b @c switch a {
-  ///   0: (A b c)
-  ///   _: (B a-1 b c)
+  /// @a @b @c let d = (b c); switch a {
+  ///   0: (A b c d)
+  ///   _: (B a-1 b c d)
   /// }
-  /// // Since `b` and `c` would be eta-reducible if linearized,
+  /// // Since `b`, `c` and `d` would be eta-reducible if linearized,
   /// // they get pushed inside the match.
   /// @a switch a {
-  ///   0: @b @c (A b c)
-  ///   _: @b @c (B a-1 b c)
+  ///   0: @b @c let d = (b c); (A b c d)
+  ///   _: @b @c let d = (b c); (B a-1 b c d)
   /// }
   /// ```
-  pub fn linearize_match_lambdas(&mut self) {
+  pub fn linearize_match_binds(&mut self) {
     for def in self.defs.values_mut() {
       for rule in def.rules.iter_mut() {
-        rule.body.linearize_match_lambdas();
+        rule.body.linearize_match_binds();
       }
     }
   }
+}
 
-  /// Linearizes all variables used in a matches' arms.
-  pub fn linearize_matches(&mut self) {
-    for def in self.defs.values_mut() {
-      for rule in def.rules.iter_mut() {
-        rule.body.linearize_matches();
-      }
-    }
+impl Term {
+  /// Linearize any binds preceding a match/switch term, up to the
+  /// first bind used in either the scrutinee or the bind.
+  pub fn linearize_match_binds(&mut self) {
+    self.linearize_match_binds_go(vec![]);
   }
 
-  /// Linearizes all variables specified in the `with` clauses of match terms.
-  pub fn linearize_match_with(&mut self) {
-    for def in self.defs.values_mut() {
-      for rule in def.rules.iter_mut() {
-        rule.body.linearize_match_with();
+  fn linearize_match_binds_go(&mut self, mut bind_terms: Vec<Term>) {
+    match self {
+      // Binding terms
+      // Extract them in case they are preceding a match.
+      Term::Lam { bod, .. } => {
+        let bod = std::mem::take(bod.as_mut());
+        let term = std::mem::replace(self, bod);
+        bind_terms.push(term);
+        self.linearize_match_binds_go(bind_terms);
+      }
+      Term::Let { val, nxt, .. }
+      | Term::Ltp { val, nxt, .. }
+      | Term::Dup { val, nxt, .. }
+      | Term::Use { val, nxt, .. } => {
+        val.linearize_match_binds_go(vec![]);
+        let nxt = std::mem::take(nxt.as_mut());
+        let term = std::mem::replace(self, nxt);
+        bind_terms.push(term);
+        self.linearize_match_binds_go(bind_terms);
+      }
+
+      // Matching terms
+      Term::Mat { .. } | Term::Swt { .. } => {
+        self.linearize_match(bind_terms);
+      }
+
+      // Others
+      // Not a match preceded by binds, so put the extracted terms back.
+      term => {
+        for child in term.children_mut() {
+          child.linearize_match_binds_go(vec![]);
+        }
+        // Recover the extracted terms
+        term.wrap_with_bind_terms(bind_terms);
       }
     }
   }
-}
 
-impl Term {
-  /// Linearize any lambdas preceding a match/switch expression.
-  ///
-  /// We push down the lambdas between the one being matched and the match expression.
-  ///
-  /// ### Example:
-  /// ```hvm
-  /// @a @b @c @d switch b {
-  ///   0: (Foo a c d)
-  ///   _: (Bar a b-1 c d)
-  /// }
-  ///
-  /// // Becomes
-  /// @a @b switch b {
-  ///   0: @c @d (Foo a c d)
-  ///   _: @c @d (Bar a b-1 c d)
-  /// }
-  /// ```
-  pub fn linearize_match_lambdas(&mut self) {
-    maybe_grow(|| match self {
-      Term::Lam { .. } => {
-        let mut term_owned = std::mem::take(self);
-        let mut term = &mut term_owned;
-        let mut lams = vec![];
-        while let Term::Lam { tag, nam, bod } = term {
-          lams.push((tag, nam));
-          term = bod.as_mut();
+  fn linearize_match(&mut self, mut bind_terms: Vec<Term>) {
+    // The used vars are any free vars in the argument,
+    // the match bind and the ctr field binds.
+    let (vars, with, mut arms) = match self {
+      Term::Mat { arg, bnd, with, arms } => {
+        let mut vars = arg.free_vars().into_keys().collect::<HashSet<_>>();
+        if let Some(bnd) = bnd {
+          vars.insert(bnd.clone());
+        }
+        for arm in arms.iter() {
+          vars.extend(arm.1.iter().flatten().cloned());
         }
 
-        let to_linearize = match term {
-          Term::Mat { arg, with, rules } if matches!(arg.as_ref(), Term::Var { .. } | Term::Era) => {
-            let arg = if let Term::Var { nam } = arg.as_ref() { Some(nam.clone()) } else { None };
-            let bodies = rules.iter_mut().map(|(_, _, body)| body).collect::<Vec<_>>();
-            Some((arg, with, bodies))
-          }
-          Term::Swt { arg, with, rules } if matches!(arg.as_ref(), Term::Var { .. } | Term::Era) => {
-            let arg = if let Term::Var { nam } = arg.as_ref() { Some(nam.clone()) } else { None };
-            let bodies = rules.iter_mut().map(|(_, body)| body).collect();
-            Some((arg, with, bodies))
-          }
-          _ => None,
-        };
+        let arms = arms.iter_mut().map(|arm| &mut arm.2).collect::<Vec<_>>();
 
-        if let Some((arg, with, mut bodies)) = to_linearize {
-          // Lambdas followed by match, push the lambdas inside the match arms.
-          // Find which lambdas will be pushed down and which have to remain.
-          let mut last_lam = 0;
-          for i in (0 .. lams.len()).rev() {
-            if let Some(lam_var) = &lams[i].1
-              && *lam_var == arg
-            {
-              last_lam = i + 1;
-              break;
-            }
-          }
+        (vars, with, arms)
+      }
+      Term::Swt { arg, bnd, with, pred, arms } => {
+        let mut vars = arg.free_vars().into_keys().collect::<HashSet<_>>();
+        if let Some(bnd) = bnd {
+          vars.insert(bnd.clone());
+        }
+        if let Some(pred) = pred {
+          vars.insert(pred.clone());
+        }
 
-          for (tag, nam) in lams[last_lam ..].iter_mut().rev() {
-            // Move the lambdas down
-            for body in bodies.iter_mut() {
-              **body = Term::Lam { tag: tag.clone(), nam: nam.clone(), bod: Box::new(std::mem::take(body)) };
-            }
-            // Remove the variable from the with clause
-            if let Some(nam) = nam {
-              with.retain(|with| with != nam);
-            }
-          }
+        let arms = arms.iter_mut().collect();
 
-          // Recursive call on the moved lambdas
-          for body in bodies.iter_mut() {
-            body.linearize_match_lambdas();
-          }
+        (vars, with, arms)
+      }
+      _ => unreachable!(),
+    };
 
-          // Reconstruct the lambdas that were not moved down
-          term_owned =
-            lams[0 .. last_lam].iter_mut().rfold(std::mem::take(term), |term, (tag, nam)| Term::Lam {
-              tag: std::mem::replace(tag, Tag::Static),
-              nam: std::mem::take(nam),
-              bod: Box::new(term),
-            });
-        } else {
-          // Not an interesting match, go back to the normal flow
-          term.linearize_match_lambdas()
+    // Move binding terms inwards, up to the first bind used in the match.
+    while let Some(term) = bind_terms.pop() {
+      // Get the binds in the term we want to push down.
+      let binds: Vec<Name> = match &term {
+        Term::Dup { bnd, .. } | Term::Ltp { bnd, .. } => bnd.iter().flatten().cloned().collect(),
+        Term::Lam { nam, .. } | Term::Let { nam, .. } | Term::Use { nam, .. } => {
+          if let Some(nam) = nam {
+            vec![nam.clone()]
+          } else {
+            vec![]
+          }
         }
+        _ => unreachable!(),
+      };
 
-        *self = term_owned;
+      if binds.iter().all(|bnd| !vars.contains(bnd)) {
+        // If possible, move term inside, wrapping around each arm.
+        for arm in arms.iter_mut() {
+          arm.wrap_with_bind_terms([term.clone()]);
+        }
+        // Since this bind doesn't exist anymore,
+        // we have to remove it from the `with` clause.
+        with.retain(|var| !binds.contains(var));
+      } else {
+        // Otherwise we stop and put this term back to be put in it's original position.
+        bind_terms.push(term);
+        break;
       }
-      _ => {
-        for child in self.children_mut() {
-          child.linearize_match_lambdas();
+    }
+
+    // Recurse
+    for arm in arms {
+      arm.linearize_match_binds_go(vec![]);
+    }
+
+    // Recover any leftover bind terms that were not moved
+    self.wrap_with_bind_terms(bind_terms);
+  }
+
+  /// Given a term `self` and a sequence of `bind_terms`, wrap `self` with those binds.
+  ///
+  /// Example:
+  /// ```hvm
+  /// self = X
+  /// match_terms = [λb *, let c = (a b); *, λd *]
+  /// ```
+  ///
+  /// becomes
+  ///
+  /// ```hvm
+  /// self = λb let c = (a b); λd X
+  /// ```
+  fn wrap_with_bind_terms(
+    &mut self,
+    bind_terms: impl IntoIterator<IntoIter = impl DoubleEndedIterator<Item = Term>>,
+  ) {
+    *self = bind_terms.into_iter().rfold(std::mem::take(self), |acc, mut term| {
+      match &mut term {
+        Term::Lam { bod: nxt, .. }
+        | Term::Let { nxt, .. }
+        | Term::Ltp { nxt, .. }
+        | Term::Dup { nxt, .. }
+        | Term::Use { nxt, .. } => {
+          *nxt.as_mut() = acc;
         }
+        _ => unreachable!(),
       }
-    })
+      term
+    });
+  }
+}
+
+/* Linearize all used vars */
+
+impl Book {
+  /// Linearizes all variables used in a matches' arms.
+  pub fn linearize_matches(&mut self) {
+    for def in self.defs.values_mut() {
+      for rule in def.rules.iter_mut() {
+        rule.body.linearize_matches();
+      }
+    }
   }
+}
 
+impl Term {
   fn linearize_matches(&mut self) {
     maybe_grow(|| {
       for child in self.children_mut() {
@@ -152,57 +207,27 @@ impl Term {
       }
     })
   }
-
-  fn linearize_match_with(&mut self) {
-    maybe_grow(|| {
-      for child in self.children_mut() {
-        child.linearize_match_with();
-      }
-    });
-    match self {
-      Term::Mat { arg: _, with, rules } => {
-        // Linearize the vars in the `with` clause, but only the used ones.
-        let with = retain_used_names(std::mem::take(with), rules.iter().map(|r| &r.2));
-        for rule in rules {
-          rule.2 =
-            with.iter().rfold(std::mem::take(&mut rule.2), |bod, nam| Term::lam(Some(nam.clone()), bod));
-        }
-        *self = Term::call(std::mem::take(self), with.into_iter().map(|nam| Term::Var { nam }));
-      }
-      Term::Swt { arg: _, with, rules } => {
-        let with = retain_used_names(std::mem::take(with), rules.iter().map(|r| &r.1));
-        for rule in rules {
-          rule.1 =
-            with.iter().rfold(std::mem::take(&mut rule.1), |bod, nam| Term::lam(Some(nam.clone()), bod));
-        }
-        *self = Term::call(std::mem::take(self), with.into_iter().map(|nam| Term::Var { nam }));
-      }
-      _ => {}
-    }
-  }
 }
 
-/// Converts free vars inside the match arms into lambdas with applications to give them the external value.
-/// Makes the rules extractable and linear (no need for dups when variable used in both rules)
+/// Converts free vars inside the match arms into lambdas with
+/// applications around the match to pass them the external value.
 ///
-/// If `lift_all_vars`, acts on all variables found in the arms,
-/// Otherwise, only lift vars that are used on more than one arm.
+/// Makes the rules extractable and linear (no need for dups even
+/// when a variable is used in multiple rules).
 ///
-/// Obs: This does not modify unscoped variables
+/// Obs: This does not modify unscoped variables.
 pub fn lift_match_vars(match_term: &mut Term) -> &mut Term {
   // Collect match arms with binds
   let arms: Vec<_> = match match_term {
-    Term::Mat { arg: _, with: _, rules } => {
+    Term::Mat { arg: _, bnd: _, with: _, arms: rules } => {
       rules.iter().map(|(_, binds, body)| (binds.iter().flatten().cloned().collect(), body)).collect()
     }
-    Term::Swt { arg: _, with: _, rules } => rules
-      .iter()
-      .map(|(ctr, body)| match ctr {
-        NumCtr::Num(_) => (vec![], body),
-        NumCtr::Succ(None) => (vec![], body),
-        NumCtr::Succ(Some(var)) => (vec![var.clone()], body),
-      })
-      .collect(),
+    Term::Swt { arg: _, bnd: _, with: _, pred, arms } => {
+      let (succ, nums) = arms.split_last_mut().unwrap();
+      let mut arms = nums.iter().map(|body| (vec![], body)).collect::<Vec<_>>();
+      arms.push((vec![pred.clone().unwrap()], succ));
+      arms
+    }
     _ => unreachable!(),
   };
 
@@ -222,18 +247,18 @@ pub fn lift_match_vars(match_term: &mut Term) -> &mut Term {
 
   // Add lambdas to the arms
   match match_term {
-    Term::Mat { arg: _, with, rules } => {
+    Term::Mat { arg: _, bnd: _, with, arms } => {
       with.retain(|with| !vars_to_lift.contains(with));
-      for rule in rules {
-        let old_body = std::mem::take(&mut rule.2);
-        rule.2 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
+      for arm in arms {
+        let old_body = std::mem::take(&mut arm.2);
+        arm.2 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
       }
     }
-    Term::Swt { arg: _, with, rules } => {
+    Term::Swt { arg: _, bnd: _, with, pred: _, arms } => {
       with.retain(|with| !vars_to_lift.contains(with));
-      for rule in rules {
-        let old_body = std::mem::take(&mut rule.1);
-        rule.1 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
+      for arm in arms {
+        let old_body = std::mem::take(arm);
+        *arm = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
       }
     }
     _ => unreachable!(),
@@ -258,6 +283,48 @@ fn get_match_reference(mut match_term: &mut Term) -> &mut Term {
   }
 }
 
+/* Linearize `with` vars  */
+
+impl Book {
+  /// Linearizes all variables specified in the `with` clauses of match terms.
+  pub fn linearize_match_with(&mut self) {
+    for def in self.defs.values_mut() {
+      for rule in def.rules.iter_mut() {
+        rule.body.linearize_match_with();
+      }
+    }
+  }
+}
+
+impl Term {
+  fn linearize_match_with(&mut self) {
+    maybe_grow(|| {
+      for child in self.children_mut() {
+        child.linearize_match_with();
+      }
+    });
+    match self {
+      Term::Mat { arg: _, bnd: _, with, arms: rules } => {
+        // Linearize the vars in the `with` clause, but only the used ones.
+        let with = retain_used_names(std::mem::take(with), rules.iter().map(|r| &r.2));
+        for rule in rules {
+          rule.2 =
+            with.iter().rfold(std::mem::take(&mut rule.2), |bod, nam| Term::lam(Some(nam.clone()), bod));
+        }
+        *self = Term::call(std::mem::take(self), with.into_iter().map(|nam| Term::Var { nam }));
+      }
+      Term::Swt { arg: _, bnd: _, with, pred: _, arms } => {
+        let with = retain_used_names(std::mem::take(with), arms.iter());
+        for arm in arms {
+          *arm = with.iter().rfold(std::mem::take(arm), |bod, nam| Term::lam(Some(nam.clone()), bod));
+        }
+        *self = Term::call(std::mem::take(self), with.into_iter().map(|nam| Term::Var { nam }));
+      }
+      _ => {}
+    }
+  }
+}
+
 /// From a Vec of variable names, return the ones that are used inside `terms`.
 fn retain_used_names<'a>(mut names: Vec<Name>, terms: impl IntoIterator<Item = &'a Term>) -> Vec<Name> {
   let mut used_names = HashSet::new();
diff --git a/src/term/transform/resugar_adts.rs b/src/term/transform/resugar_adts.rs
index 15ae0d1ac..885c32734 100644
--- a/src/term/transform/resugar_adts.rs
+++ b/src/term/transform/resugar_adts.rs
@@ -268,13 +268,9 @@ impl Term {
     let arms = arms.into_iter().collect::<Vec<_>>();
 
     *self = if let Some(bind) = bind {
-      Term::Let {
-        nam: Some(arg.clone()),
-        val: Box::new(bind),
-        nxt: Box::new(Term::Mat { arg: Box::new(Term::Var { nam: arg }), with: vec![], rules: arms }),
-      }
+      Term::Mat { arg: Box::new(bind), bnd: Some(arg.clone()), with: vec![], arms }
     } else {
-      Term::Mat { arg: Box::new(Term::Var { nam: arg }), with: vec![], rules: arms }
+      Term::Mat { arg: Box::new(Term::Var { nam: arg.clone() }), bnd: Some(arg.clone()), with: vec![], arms }
     };
   }
 }
diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs
index f2268937d..b9bf7a3ed 100644
--- a/tests/golden_tests.rs
+++ b/tests/golden_tests.rs
@@ -238,13 +238,12 @@ fn simplify_matches() {
     ctx.set_entrypoint();
     ctx.book.encode_adts(AdtEncoding::TaggedScott);
     ctx.fix_match_defs()?;
-    ctx.book.apply_use();
     ctx.book.encode_builtins();
     ctx.resolve_refs()?;
     ctx.fix_match_terms()?;
     ctx.desugar_match_defs()?;
     ctx.check_unbound_vars()?;
-    ctx.book.linearize_match_lambdas();
+    ctx.book.linearize_match_binds();
     ctx.book.linearize_match_with();
     ctx.check_unbound_vars()?;
     ctx.prune(false, AdtEncoding::TaggedScott);
@@ -273,17 +272,18 @@ fn encode_pattern_match() {
       ctx.set_entrypoint();
       ctx.book.encode_adts(adt_encoding);
       ctx.fix_match_defs()?;
-      ctx.book.apply_use();
       ctx.book.encode_builtins();
       ctx.resolve_refs()?;
       ctx.fix_match_terms()?;
       ctx.desugar_match_defs()?;
       ctx.check_unbound_vars()?;
-      ctx.book.linearize_match_lambdas();
+      ctx.book.linearize_match_binds();
       ctx.book.linearize_match_with();
       ctx.book.encode_matches(adt_encoding);
       ctx.check_unbound_vars()?;
       ctx.book.make_var_names_unique();
+      ctx.book.apply_use();
+      ctx.book.make_var_names_unique();
       ctx.book.linearize_vars();
       ctx.prune(false, adt_encoding);
 
diff --git a/tests/golden_tests/compile_file/switch_in_switch_arg.hvm b/tests/golden_tests/compile_file/switch_in_switch_arg.hvm
index c328319d4..f392d4890 100644
--- a/tests/golden_tests/compile_file/switch_in_switch_arg.hvm
+++ b/tests/golden_tests/compile_file/switch_in_switch_arg.hvm
@@ -1,4 +1,4 @@
-main x = switch (switch x {0: 0; _: x-1}) {
+main x = switch x = (switch x {0: 0; _: x-1}) {
   0: 0
   _: x
 }
diff --git a/tests/golden_tests/compile_term/match.hvm b/tests/golden_tests/compile_term/match.hvm
index 738e3736f..ac445c92a 100644
--- a/tests/golden_tests/compile_term/match.hvm
+++ b/tests/golden_tests/compile_term/match.hvm
@@ -1,4 +1,4 @@
-switch (+ 0 1) {
+switch x = (+ 0 1) {
   0: λt λf t
   _: λ* λt λf f // The term to hvmc function assumes the pred variable is already detached from the match
 }
\ No newline at end of file
diff --git a/tests/golden_tests/desugar_file/switch_with_use.hvm b/tests/golden_tests/desugar_file/switch_with_use.hvm
new file mode 100644
index 000000000..4e9068d63
--- /dev/null
+++ b/tests/golden_tests/desugar_file/switch_with_use.hvm
@@ -0,0 +1,6 @@
+// Test manual linearization of a use term
+main =
+  @x @y use z = (x y); @a @b @c switch a with z {
+    0: z
+    _: (a-1 z)
+  }
diff --git a/tests/golden_tests/desugar_file/use_switch.hvm b/tests/golden_tests/desugar_file/use_switch.hvm
deleted file mode 100644
index af77b9310..000000000
--- a/tests/golden_tests/desugar_file/use_switch.hvm
+++ /dev/null
@@ -1,5 +0,0 @@
-main =
-  @a @b @c use e = (b c) switch a with e {
-    0: e
-    _: (a-1 e)
-  }
diff --git a/tests/golden_tests/encode_pattern_match/match_auto_linearization.hvm b/tests/golden_tests/encode_pattern_match/match_auto_linearization.hvm
new file mode 100644
index 000000000..df3ad5a2c
--- /dev/null
+++ b/tests/golden_tests/encode_pattern_match/match_auto_linearization.hvm
@@ -0,0 +1,36 @@
+// Given a match/switch term preceded by a sequence of terms with binds (lambda, let, use, etc),
+// by default we linearize all bindings up to the first one that appears in the match "header".
+
+switch_linearization =
+  @a
+  @b
+  let c = 2;
+  let {c1 c2} = c;
+  use d = (a, b);
+  let (e, f) = d;
+  switch a {
+    0: (b c c1 c2 d e f)
+    _: (a-1 b c c1 c2 d e f)
+  }
+
+match_linearization =
+  @a
+  @b
+  let c = 2;
+  let {c1 c2} = c;
+  use d = (a, b);
+  let (e, f) = d;
+  match a {
+    Nat.zero: (b c c1 c2 d e f)
+    Nat.succ: (a.pred b c c1 c2 d e f)
+  }
+
+switch_shadowed_field = @a @a-1 switch a {
+  0: a-1
+  _: a-1
+}
+
+match_shadowed_field = @a @a.head @a.tail match a {
+  List.nil: (List.cons a.head a.tail)
+  List.cons: (List.cons a.head a.tail)
+}
\ No newline at end of file
diff --git a/tests/golden_tests/encode_pattern_match/switch_in_switch_arg.hvm b/tests/golden_tests/encode_pattern_match/switch_in_switch_arg.hvm
index c328319d4..f392d4890 100644
--- a/tests/golden_tests/encode_pattern_match/switch_in_switch_arg.hvm
+++ b/tests/golden_tests/encode_pattern_match/switch_in_switch_arg.hvm
@@ -1,4 +1,4 @@
-main x = switch (switch x {0: 0; _: x-1}) {
+main x = switch x = (switch x {0: 0; _: x-1}) {
   0: 0
   _: x
 }
diff --git a/tests/golden_tests/run_file/kind_compiled_tree_sum.hvm b/tests/golden_tests/run_file/kind_compiled_tree_sum.hvm
new file mode 100644
index 000000000..fe39036ad
--- /dev/null
+++ b/tests/golden_tests/run_file/kind_compiled_tree_sum.hvm
@@ -0,0 +1,43 @@
+//WARNING: unsolved metas.
+//WARNING: unsolved metas.
+_Char = 0
+_List = λ_T 0
+_List.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
+_List.nil = λ_P λ_cons λ_nil _nil
+_Nat = 0
+_Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
+_Nat.zero = λ_P λ_succ λ_zero _zero
+_String = (_List _Char)
+_String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
+_String.nil = λ_P λ_cons λ_nil _nil
+_Tree = λ_A 0
+
+_Tree.fold =
+  λ_bm λ_nd λ_lf
+  let _bm.P = 0;
+  let _bm.node = λ_bm.val λ_bm.lft λ_bm.rgt λ_nd λ_lf (((_nd _bm.val) (((_Tree.fold _bm.lft) _nd) _lf)) (((_Tree.fold _bm.rgt) _nd) _lf));
+  let _bm.leaf = λ_nd λ_lf _lf;
+  ((((let _bm = _bm (_bm _bm.P) _bm.node) _bm.leaf) _nd) _lf)
+
+_Tree.gen = λ_n λ_x switch _n = _n {
+  0: _Tree.leaf
+  _: let _n-1 = _n-1 (
+    _Tree.node
+    _x
+    (_Tree.gen _n-1 (+ (* _x 2) 1))
+    (_Tree.gen _n-1 (+ (* _x 2) 2))
+  )
+}
+
+_Tree.leaf = λ_P λ_node λ_leaf _leaf
+
+_Tree.node = λ_val λ_lft λ_rgt λ_P λ_node λ_leaf (((_node _val) _lft) _rgt)
+
+_Tree.sum = λ_x
+  let _x.P = 0
+  let _x.node = λ_x.val λ_x.lft λ_x.rgt (+ _x.val (+ _x.lft _x.rgt))
+  let _x.leaf = 0
+  ((let _x = _x (_Tree.fold _x) _x.node) _x.leaf)
+
+main = (_Tree.sum ((_Tree.gen 16) 0))
+
diff --git a/tests/golden_tests/run_file/list_take.hvm b/tests/golden_tests/run_file/list_take.hvm
index 8befd00b7..8122f6eff 100644
--- a/tests/golden_tests/run_file/list_take.hvm
+++ b/tests/golden_tests/run_file/list_take.hvm
@@ -1,5 +1,5 @@
 Take_ n list =
-  switch (== n 0) {
+  switch _ = (== n 0) {
   | 0: (Take n list)
   | _: []
   }
diff --git a/tests/golden_tests/run_file/list_to_tree.hvm b/tests/golden_tests/run_file/list_to_tree.hvm
index fb248552a..fb03e12ae 100644
--- a/tests/golden_tests/run_file/list_to_tree.hvm
+++ b/tests/golden_tests/run_file/list_to_tree.hvm
@@ -3,7 +3,7 @@ List.len.go [] count = count
 List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1))
 
 Take.go n list =
-  switch (== n 0) {
+  switch _ = (== n 0) {
   | 0: (Take n list)
   | _: []
   }
@@ -11,7 +11,7 @@ Take n [] = []
 Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs))
 
 Drop.go n list =
-  switch (== n 0) {
+  switch _ = (== n 0) {
   | 0: (Drop n list)
   | _: list
   }
diff --git a/tests/golden_tests/run_file/match.hvm b/tests/golden_tests/run_file/match.hvm
index a4e1e1307..4875af666 100644
--- a/tests/golden_tests/run_file/match.hvm
+++ b/tests/golden_tests/run_file/match.hvm
@@ -1,5 +1,5 @@
 main =
-  switch (+ 0 1) {
+  switch _ = (+ 0 1) {
     0: λt λf t
     _: λt λf f
   }
\ No newline at end of file
diff --git a/tests/golden_tests/run_file/merge_sort.hvm b/tests/golden_tests/run_file/merge_sort.hvm
index 0288b3293..ff9b72c25 100644
--- a/tests/golden_tests/run_file/merge_sort.hvm
+++ b/tests/golden_tests/run_file/merge_sort.hvm
@@ -7,7 +7,7 @@ sort (Node a b) = (merge (sort a) (sort b))
 merge (Nil) b = b
 merge (Cons x xs) (Nil) = (Cons x xs)
 merge (Cons x xs) (Cons y ys) = 
-  let t = switch (< x y) {
+  let t = switch _ = (< x y) {
     0: λaλbλcλt(t c a b)
     _: λaλbλcλt(t a b c)
   }
diff --git a/tests/golden_tests/run_lazy/list_take.hvm b/tests/golden_tests/run_lazy/list_take.hvm
index 8befd00b7..8122f6eff 100644
--- a/tests/golden_tests/run_lazy/list_take.hvm
+++ b/tests/golden_tests/run_lazy/list_take.hvm
@@ -1,5 +1,5 @@
 Take_ n list =
-  switch (== n 0) {
+  switch _ = (== n 0) {
   | 0: (Take n list)
   | _: []
   }
diff --git a/tests/golden_tests/run_lazy/list_to_tree.hvm b/tests/golden_tests/run_lazy/list_to_tree.hvm
index fb248552a..fb03e12ae 100644
--- a/tests/golden_tests/run_lazy/list_to_tree.hvm
+++ b/tests/golden_tests/run_lazy/list_to_tree.hvm
@@ -3,7 +3,7 @@ List.len.go [] count = count
 List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1))
 
 Take.go n list =
-  switch (== n 0) {
+  switch _ = (== n 0) {
   | 0: (Take n list)
   | _: []
   }
@@ -11,7 +11,7 @@ Take n [] = []
 Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs))
 
 Drop.go n list =
-  switch (== n 0) {
+  switch _ = (== n 0) {
   | 0: (Drop n list)
   | _: list
   }
diff --git a/tests/golden_tests/run_lazy/match.hvm b/tests/golden_tests/run_lazy/match.hvm
index a4e1e1307..4875af666 100644
--- a/tests/golden_tests/run_lazy/match.hvm
+++ b/tests/golden_tests/run_lazy/match.hvm
@@ -1,5 +1,5 @@
 main =
-  switch (+ 0 1) {
+  switch _ = (+ 0 1) {
     0: λt λf t
     _: λt λf f
   }
\ No newline at end of file
diff --git a/tests/golden_tests/run_lazy/merge_sort.hvm b/tests/golden_tests/run_lazy/merge_sort.hvm
index 0288b3293..ff9b72c25 100644
--- a/tests/golden_tests/run_lazy/merge_sort.hvm
+++ b/tests/golden_tests/run_lazy/merge_sort.hvm
@@ -7,7 +7,7 @@ sort (Node a b) = (merge (sort a) (sort b))
 merge (Nil) b = b
 merge (Cons x xs) (Nil) = (Cons x xs)
 merge (Cons x xs) (Cons y ys) = 
-  let t = switch (< x y) {
+  let t = switch _ = (< x y) {
     0: λaλbλcλt(t c a b)
     _: λaλbλcλt(t a b c)
   }
diff --git a/tests/snapshots/cli__desugar_linearize_matches.hvm.snap b/tests/snapshots/cli__desugar_linearize_matches.hvm.snap
index 75607e16f..274eedf3b 100644
--- a/tests/snapshots/cli__desugar_linearize_matches.hvm.snap
+++ b/tests/snapshots/cli__desugar_linearize_matches.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/desugar_linearize_matches.hvm
 ---
-(main) = λa switch a { 0: λb b; _: λ* λd d }
+(main) = λa switch a = a { 0: λb b; _: λ* λd d }
diff --git a/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap b/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap
index a7cc73076..1b80f4f0a 100644
--- a/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap
+++ b/tests/snapshots/cli__desugar_linearize_matches_extra.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/desugar_linearize_matches_extra.hvm
 ---
-(main) = λa λb λc (switch a { 0: λd λ* d; _: λ* λ* λh h } b c)
+(main) = λa λb λc (switch a = a { 0: λd λ* d; _: λ* λ* λh h } b c)
diff --git a/tests/snapshots/cli__run_pretty.hvm.snap b/tests/snapshots/cli__run_pretty.hvm.snap
index 9383d0a09..035564803 100644
--- a/tests/snapshots/cli__run_pretty.hvm.snap
+++ b/tests/snapshots/cli__run_pretty.hvm.snap
@@ -2,10 +2,10 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/cli/run_pretty.hvm
 ---
-λ* λa switch a {
-  0: λb switch b {
-    0: "ba"
-    _: "ta"
-  }
-  _: λ* "ata"
+λ* λa switch a = a {
+  0: λb switch b = b {
+      0: "ba";
+      _: "ta";
+    };
+  _: λ* "ata";
 }
diff --git a/tests/snapshots/compile_file__switch_all_patterns.hvm.snap b/tests/snapshots/compile_file__switch_all_patterns.hvm.snap
index 7c7f70e78..9cbd3df42 100644
--- a/tests/snapshots/compile_file__switch_all_patterns.hvm.snap
+++ b/tests/snapshots/compile_file__switch_all_patterns.hvm.snap
@@ -3,15 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/switch_all_patterns.hvm
 ---
 Errors:
-In definition 'succ':
-  Malformed 'switch' expression. Expected case '0', found '_'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case.
-In definition 'succ_zero':
-  Malformed 'switch' expression. Expected case '0', found '_'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case.
-In definition 'succ_zero_succ':
-  Malformed 'switch' expression. Expected case '0', found '_'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case.
-In definition 'zero_succ_succ':
-  Extra arms in 'switch' expression. No rules should come after the default.
-In definition 'zero_succ_zero':
-  Extra arms in 'switch' expression. No rules should come after the default.
-In definition 'zero_zero_succ':
-  Malformed 'switch' expression. Expected case '1', found '0'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case.
+In tests/golden_tests/compile_file/switch_all_patterns.hvm :
+- expected: 0
+- detected:
+  7 |   _: x-1
diff --git a/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap b/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap
index 846c6614a..17b5cb269 100644
--- a/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap
+++ b/tests/snapshots/compile_file__switch_in_switch_arg.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/switch_in_switch_arg.hvm
 ---
-@main = ({3 a ?<#0 (b b) ?<#0 (* a) c>>} c)
+@main = (?<#0 (a a) ?<#0 (<+ #1 b> b) c>> c)
diff --git a/tests/snapshots/desugar_file__switch_with_use.hvm.snap b/tests/snapshots/desugar_file__switch_with_use.hvm.snap
new file mode 100644
index 000000000..1af160866
--- /dev/null
+++ b/tests/snapshots/desugar_file__switch_with_use.hvm.snap
@@ -0,0 +1,5 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/desugar_file/switch_with_use.hvm
+---
+(main) = λa λb λc (switch a = c { 0: λd λ* λ* d; _: λg λh λ* λ* (g h) } (a b))
diff --git a/tests/snapshots/desugar_file__use_switch.hvm.snap b/tests/snapshots/desugar_file__use_switch.hvm.snap
deleted file mode 100644
index 1d58eb147..000000000
--- a/tests/snapshots/desugar_file__use_switch.hvm.snap
+++ /dev/null
@@ -1,5 +0,0 @@
----
-source: tests/golden_tests.rs
-input_file: tests/golden_tests/desugar_file/use_switch.hvm
----
-(main) = λa λb λc (switch a { 0: λd d; _: λe λf (e f) } (b c))
diff --git a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap
index a57e57925..a3380adc0 100644
--- a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap
@@ -7,7 +7,7 @@ TaggedScott:
 
 (Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f
 
-(Fn3) = λa λ* let (c, *) = a; switch c { 0: 0; _: λe (+ e 1) }
+(Fn3) = λa λ* let (c, *) = a; switch %arg0.0 = c { 0: 0; _: λe (+ e 1) }
 
 (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
 
@@ -16,6 +16,6 @@ Scott:
 
 (Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f
 
-(Fn3) = λa λ* let (c, *) = a; switch c { 0: 0; _: λe (+ e 1) }
+(Fn3) = λa λ* let (c, *) = a; switch %arg0.0 = c { 0: 0; _: λe (+ e 1) }
 
 (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
index 2523dd836..f08086d73 100644
--- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_lambda.hvm.snap
@@ -3,14 +3,14 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm
 ---
 TaggedScott:
-(main) = (#Maybe ((Some 1) λ$x * #Maybe λb b) $x)
+(main) = (#Maybe ((Some 1) λ$x * #Maybe λa a) $x)
 
 (None) = #Maybe λa #Maybe λ* a
 
 (Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
 
 Scott:
-(main) = (Some 1 λ$x * λb b $x)
+(main) = (Some 1 λ$x * λa a $x)
 
 (None) = λa λ* a
 
diff --git a/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap b/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
index ed3896e96..7bbad68c8 100644
--- a/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_adt_unscoped_var.hvm.snap
@@ -3,9 +3,9 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm
 ---
 TaggedScott:
-(Foo) = λ$x #Maybe ((Some 1) $x #Maybe λb b)
+(Foo) = λ$x #Maybe ((Some 1) $x #Maybe λa a)
 
-(Bar) = (#Maybe ((Some 1) $x #Maybe λb b) λ$x *)
+(Bar) = (#Maybe ((Some 1) $x #Maybe λa a) λ$x *)
 
 (main) = *
 
@@ -14,9 +14,9 @@ TaggedScott:
 (Some) = λa #Maybe λ* #Maybe λc #Maybe (c a)
 
 Scott:
-(Foo) = λ$x (Some 1 $x λb b)
+(Foo) = λ$x (Some 1 $x λa a)
 
-(Bar) = (Some 1 $x λb b λ$x *)
+(Bar) = (Some 1 $x λa a λ$x *)
 
 (main) = *
 
diff --git a/tests/snapshots/encode_pattern_match__match_auto_linearization.hvm.snap b/tests/snapshots/encode_pattern_match__match_auto_linearization.hvm.snap
new file mode 100644
index 000000000..a4b3a4bb2
--- /dev/null
+++ b/tests/snapshots/encode_pattern_match__match_auto_linearization.hvm.snap
@@ -0,0 +1,37 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/encode_pattern_match/match_auto_linearization.hvm
+---
+TaggedScott:
+(switch_linearization) = λa switch a = a { 0: λb let {b b_2 b_3} = b; let {c c_2} = 2; let {d e} = c; let (f, g) = (0, b); (b_2 c_2 d e (0, b_3) f g); _: λh let {h h_2 h_3} = h; λi let {i i_2 i_3} = i; let {j j_2} = 2; let {k l} = j; let (m, n) = ((+ h 1), i); (h_2 i_2 j_2 k l ((+ h_3 1), i_3) m n) }
+
+(match_linearization) = λa #Nat (a #Nat λb let {b b_2 b_3} = b; λc let {c c_2 c_3} = c; let {d d_2} = 2; let {e f} = d; let (g, h) = ((Nat.succ b), c); (b_2 c_2 d_2 e f ((Nat.succ b_3), c_3) g h) λi let {i i_2 i_3} = i; let {j j_2} = 2; let {k l} = j; let (m, n) = (Nat.zero, i); (i_2 j_2 k l (Nat.zero, i_3) m n))
+
+(switch_shadowed_field) = λa λb switch a = a { 0: b; _: λc c }
+
+(match_shadowed_field) = λa λb λc #List (a #List λd #List λe (List.cons d e) (List.cons b c))
+
+(List.cons) = λa λb #List λc #List λ* #List (c a b)
+
+(List.nil) = #List λ* #List λb b
+
+(Nat.succ) = λa #Nat λb #Nat λ* #Nat (b a)
+
+(Nat.zero) = #Nat λ* #Nat λb b
+
+Scott:
+(switch_linearization) = λa switch a = a { 0: λb let {b b_2 b_3} = b; let {c c_2} = 2; let {d e} = c; let (f, g) = (0, b); (b_2 c_2 d e (0, b_3) f g); _: λh let {h h_2 h_3} = h; λi let {i i_2 i_3} = i; let {j j_2} = 2; let {k l} = j; let (m, n) = ((+ h 1), i); (h_2 i_2 j_2 k l ((+ h_3 1), i_3) m n) }
+
+(match_linearization) = λa (a λb let {b b_2 b_3} = b; λc let {c c_2 c_3} = c; let {d d_2} = 2; let {e f} = d; let (g, h) = ((Nat.succ b), c); (b_2 c_2 d_2 e f ((Nat.succ b_3), c_3) g h) λi let {i i_2 i_3} = i; let {j j_2} = 2; let {k l} = j; let (m, n) = (Nat.zero, i); (i_2 j_2 k l (Nat.zero, i_3) m n))
+
+(switch_shadowed_field) = λa λb switch a = a { 0: b; _: λc c }
+
+(match_shadowed_field) = λa λb λc (a λd λe (List.cons d e) (List.cons b c))
+
+(List.cons) = λa λb λc λ* (c a b)
+
+(List.nil) = λ* λb b
+
+(Nat.succ) = λa λb λ* (b a)
+
+(Nat.zero) = λ* λb b
diff --git a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap
index 652c4f68b..0be438168 100644
--- a/tests/snapshots/encode_pattern_match__match_bind.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_bind.hvm.snap
@@ -3,11 +3,11 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_bind.hvm
 ---
 TaggedScott:
-(cheese) = let {a a_2} = (+ 2 3); switch a { 0: 653323; _: λb (+ a_2 b) }
+(cheese) = switch num = (+ 2 3) { 0: 653323; _: λa let {a a_2} = a; (+ (+ a 1) a_2) }
 
 (main) = cheese
 
 Scott:
-(cheese) = let {a a_2} = (+ 2 3); switch a { 0: 653323; _: λb (+ a_2 b) }
+(cheese) = switch num = (+ 2 3) { 0: 653323; _: λa let {a a_2} = a; (+ (+ a 1) a_2) }
 
 (main) = cheese
diff --git a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
index 87cbd0a6b..011cd219d 100644
--- a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
@@ -3,9 +3,9 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm
 ---
 TaggedScott:
-(Parse) = λa λb (#String (b #String λc #String λd λe (switch (- c 10) { 0: λg λh (Ok (0, h, g)); _: λi λj λk (switch (- i 29) { 0: λm λn (Ok (40, n, m)); _: λo λp λq (switch o { 0: λr λs (Ok (41, s, r)); _: λt λu λv (Err ((String.cons (+ t 42) v), u)) } p q) } j k) } e d) λw (Err (String.nil, w))) a)
+(Parse) = λa λb (#String (b #String λc #String λd λe (switch %arg1.head = (- c 10) { 0: λf λg (Ok (0, g, f)); _: λh λi λj (switch %arg1.head = (- h 29) { 0: λk λl (Ok (40, l, k)); _: λm λn λo (switch %arg1.head = m { 0: λp λq (Ok (41, q, p)); _: λr λs λt (Err ((String.cons (+ r 42) t), s)) } n o) } i j) } e d) λu (Err (String.nil, u))) a)
 
-(main) = #Result_ ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result_ λd let (e, f, g) = d; (e, (Parse g f)) #Result_ λh (Err h))
+(main) = #Result_ ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result_ λc let (d, e, f) = c; (d, (Parse f e)) #Result_ λg (Err g))
 
 (String.cons) = λa λb #String λc #String λ* #String (c a b)
 
@@ -16,9 +16,9 @@ TaggedScott:
 (Err) = λa #Result_ λ* #Result_ λc #Result_ (c a)
 
 Scott:
-(Parse) = λa λb (b λc λd λe (switch (- c 10) { 0: λg λh (Ok (0, h, g)); _: λi λj λk (switch (- i 29) { 0: λm λn (Ok (40, n, m)); _: λo λp λq (switch o { 0: λr λs (Ok (41, s, r)); _: λt λu λv (Err ((String.cons (+ t 42) v), u)) } p q) } j k) } e d) λw (Err (String.nil, w)) a)
+(Parse) = λa λb (b λc λd λe (switch %arg1.head = (- c 10) { 0: λf λg (Ok (0, g, f)); _: λh λi λj (switch %arg1.head = (- h 29) { 0: λk λl (Ok (40, l, k)); _: λm λn λo (switch %arg1.head = m { 0: λp λq (Ok (41, q, p)); _: λr λs λt (Err ((String.cons (+ r 42) t), s)) } n o) } i j) } e d) λu (Err (String.nil, u)) a)
 
-(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f, g) = d; (e, (Parse g f)) λh (Err h))
+(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λc let (d, e, f) = c; (d, (Parse f e)) λg (Err g))
 
 (String.cons) = λa λb λc λ* (c a b)
 
diff --git a/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap
index 858d4f8cb..e18529fe5 100644
--- a/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_num_pred.hvm.snap
@@ -3,23 +3,23 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_num_pred.hvm
 ---
 TaggedScott:
-(pred) = λa switch a { 0: 0; _: λb b }
+(pred) = λa switch n = a { 0: 0; _: λb b }
 
-(pred2) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc c } }
+(pred2) = λa switch n = a { 0: 0; _: λb switch %x = b { 0: 0; _: λc c } }
 
-(pred3) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc switch c { 0: 0; _: λd (- (+ d 3) 3) } } }
+(pred3) = λa switch %arg0 = a { 0: 0; _: λb switch %arg0 = b { 0: 0; _: λc switch %arg0 = c { 0: 0; _: λd (- (+ d 3) 3) } } }
 
-(zero) = λa switch a { 0: 1; _: λb switch b { 0: 0; _: λ* 0 } }
+(zero) = λa switch %arg0 = a { 0: 1; _: λb switch %arg0 = b { 0: 0; _: λ* 0 } }
 
 (main) = *
 
 Scott:
-(pred) = λa switch a { 0: 0; _: λb b }
+(pred) = λa switch n = a { 0: 0; _: λb b }
 
-(pred2) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc c } }
+(pred2) = λa switch n = a { 0: 0; _: λb switch %x = b { 0: 0; _: λc c } }
 
-(pred3) = λa switch a { 0: 0; _: λb switch b { 0: 0; _: λc switch c { 0: 0; _: λd (- (+ d 3) 3) } } }
+(pred3) = λa switch %arg0 = a { 0: 0; _: λb switch %arg0 = b { 0: 0; _: λc switch %arg0 = c { 0: 0; _: λd (- (+ d 3) 3) } } }
 
-(zero) = λa switch a { 0: 1; _: λb switch b { 0: 0; _: λ* 0 } }
+(zero) = λa switch %arg0 = a { 0: 1; _: λb switch %arg0 = b { 0: 0; _: λ* 0 } }
 
 (main) = *
diff --git a/tests/snapshots/encode_pattern_match__switch_in_switch_arg.hvm.snap b/tests/snapshots/encode_pattern_match__switch_in_switch_arg.hvm.snap
index 07fcdb48d..d2db2dd4c 100644
--- a/tests/snapshots/encode_pattern_match__switch_in_switch_arg.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__switch_in_switch_arg.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/switch_in_switch_arg.hvm
 ---
 TaggedScott:
-(main) = λa let {a a_2} = a; switch switch a_2 { 0: 0; _: λb b } { 0: 0; _: λ* a }
+(main) = λa switch x = switch x = a { 0: 0; _: λb b } { 0: 0; _: λc (+ c 1) }
 
 Scott:
-(main) = λa let {a a_2} = a; switch switch a_2 { 0: 0; _: λb b } { 0: 0; _: λ* a }
+(main) = λa switch x = switch x = a { 0: 0; _: λb b } { 0: 0; _: λc (+ c 1) }
diff --git a/tests/snapshots/readback_lnet__match.hvm.snap b/tests/snapshots/readback_lnet__match.hvm.snap
index 28aa43d61..d6f1f78e2 100644
--- a/tests/snapshots/readback_lnet__match.hvm.snap
+++ b/tests/snapshots/readback_lnet__match.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/readback_lnet/match.hvm
 ---
-let c = 1; switch c { 0: λa a; _: c-1 }
+let c = 1; switch c = c { 0: λa a; _: c-1 }
diff --git a/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap b/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap
index 233193f75..4ae1dd55d 100644
--- a/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap
+++ b/tests/snapshots/run_file__adt_match_wrong_tag.hvm.snap
@@ -7,11 +7,11 @@ Warnings:
 During readback:
   Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'.
 
-λa match a { Some: #Option (#wrong_tag λb b a.val); None: * }
+λa match a = a { Some: #Option (#wrong_tag λb b a.val); None: * }
 
 Strict mode:
 Warnings:
 During readback:
   Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'.
 
-λa match a { Some: #Option (#wrong_tag λb b a.val); None: * }
+λa match a = a { Some: #Option (#wrong_tag λb b a.val); None: * }
diff --git a/tests/snapshots/run_file__adt_option_and.hvm.snap b/tests/snapshots/run_file__adt_option_and.hvm.snap
index 4c869ce27..5c5aff0b3 100644
--- a/tests/snapshots/run_file__adt_option_and.hvm.snap
+++ b/tests/snapshots/run_file__adt_option_and.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/adt_option_and.hvm
 ---
 Lazy mode:
-λa match a { Some: λc match c { Some: (Some (a.val, c.val)); None: None }; None: λ* None }
+λa match a = a { Some: λc match c = c { Some: (Some (a.val, c.val)); None: None }; None: λ* None }
 
 Strict mode:
-λa match a { Some: λc (match c { Some: λe (Some (e, c.val)); None: λ* None } a.val); None: λ* None }
+λa match a = a { Some: λc (match c = c { Some: λe (Some (e, c.val)); None: λ* None } a.val); None: λ* None }
diff --git a/tests/snapshots/run_file__adt_wrong_tag.hvm.snap b/tests/snapshots/run_file__adt_wrong_tag.hvm.snap
index 59263545e..12f5bc95e 100644
--- a/tests/snapshots/run_file__adt_wrong_tag.hvm.snap
+++ b/tests/snapshots/run_file__adt_wrong_tag.hvm.snap
@@ -7,11 +7,11 @@ Warnings:
 During readback:
   Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'.
 
-λa match a { Some: #Option (#wrong_tag λb b a.val); None: * }
+λa match a = a { Some: #Option (#wrong_tag λb b a.val); None: * }
 
 Strict mode:
 Warnings:
 During readback:
   Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'.
 
-λa match a { Some: #Option (#wrong_tag λb b a.val); None: * }
+λa match a = a { Some: #Option (#wrong_tag λb b a.val); None: * }
diff --git a/tests/snapshots/run_file__kind_compiled_tree_sum.hvm.snap b/tests/snapshots/run_file__kind_compiled_tree_sum.hvm.snap
new file mode 100644
index 000000000..be161b144
--- /dev/null
+++ b/tests/snapshots/run_file__kind_compiled_tree_sum.hvm.snap
@@ -0,0 +1,9 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/run_file/kind_compiled_tree_sum.hvm
+---
+Lazy mode:
+2147385345
+
+Strict mode:
+2147385345
diff --git a/tests/snapshots/run_file__linearize_match.hvm.snap b/tests/snapshots/run_file__linearize_match.hvm.snap
index b3b7f7812..befca3906 100644
--- a/tests/snapshots/run_file__linearize_match.hvm.snap
+++ b/tests/snapshots/run_file__linearize_match.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/linearize_match.hvm
 ---
 Lazy mode:
-λa λb switch a { 0: b; _: (+ a-1 b) }
+λa switch a = a { 0: λb b; _: λd (+ a-1 d) }
 
 Strict mode:
-λa switch a { 0: λb b; _: λd (+ a-1 d) }
+λa switch a = a { 0: λb b; _: λd (+ a-1 d) }
diff --git a/tests/snapshots/run_file__match_mult_linearization.hvm.snap b/tests/snapshots/run_file__match_mult_linearization.hvm.snap
index fba3bfcc9..778ca5364 100644
--- a/tests/snapshots/run_file__match_mult_linearization.hvm.snap
+++ b/tests/snapshots/run_file__match_mult_linearization.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/match_mult_linearization.hvm
 ---
 Lazy mode:
-λa switch a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) }
+λa switch a = a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) }
 
 Strict mode:
-λa switch a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) }
+λa switch a = a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) }
diff --git a/tests/snapshots/run_file__num_match_missing_var.hvm.snap b/tests/snapshots/run_file__num_match_missing_var.hvm.snap
index 02e15097b..73644b09e 100644
--- a/tests/snapshots/run_file__num_match_missing_var.hvm.snap
+++ b/tests/snapshots/run_file__num_match_missing_var.hvm.snap
@@ -4,15 +4,15 @@ input_file: tests/golden_tests/run_file/num_match_missing_var.hvm
 ---
 Lazy mode:
 Errors:
-In definition 'if2':
-  Extra arms in 'switch' expression. No rules should come after the default.
-In definition 'if3':
-  Extra arms in 'switch' expression. No rules should come after the default.
+In tests/golden_tests/run_file/num_match_missing_var.hvm :
+- expected: '}'
+- detected:
+  7 |   _: f
 
 
 Strict mode:
 Errors:
-In definition 'if2':
-  Extra arms in 'switch' expression. No rules should come after the default.
-In definition 'if3':
-  Extra arms in 'switch' expression. No rules should come after the default.
+In tests/golden_tests/run_file/num_match_missing_var.hvm :
+- expected: '}'
+- detected:
+  7 |   _: f
diff --git a/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap b/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap
index 9562beb4d..df976ce70 100644
--- a/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap
+++ b/tests/snapshots/run_lazy__adt_match_wrong_tag.hvm.snap
@@ -6,4 +6,4 @@ Warnings:
 During readback:
   Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'.
 
-λa match a { Some: #Option (#wrong_tag λb b a.val); None: * }
+λa match a = a { Some: #Option (#wrong_tag λb b a.val); None: * }
diff --git a/tests/snapshots/run_lazy__adt_option_and.hvm.snap b/tests/snapshots/run_lazy__adt_option_and.hvm.snap
index f7a805bc7..1d19d57d9 100644
--- a/tests/snapshots/run_lazy__adt_option_and.hvm.snap
+++ b/tests/snapshots/run_lazy__adt_option_and.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_lazy/adt_option_and.hvm
 ---
-λa match a { Some: λc match c { Some: (Some (a.val, c.val)); None: None }; None: λ* None }
+λa match a = a { Some: λc match c = c { Some: (Some (a.val, c.val)); None: None }; None: λ* None }
diff --git a/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap b/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap
index e5d8d336c..808a023c2 100644
--- a/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap
+++ b/tests/snapshots/run_lazy__adt_wrong_tag.hvm.snap
@@ -6,4 +6,4 @@ Warnings:
 During readback:
   Unexpected tag found during Adt readback, expected '#Option', but found '#wrong_tag'.
 
-λa match a { Some: #Option (#wrong_tag λb b a.val); None: * }
+λa match a = a { Some: #Option (#wrong_tag λb b a.val); None: * }
diff --git a/tests/snapshots/run_lazy__linearize_match.hvm.snap b/tests/snapshots/run_lazy__linearize_match.hvm.snap
index 904172dd5..6cc984ce6 100644
--- a/tests/snapshots/run_lazy__linearize_match.hvm.snap
+++ b/tests/snapshots/run_lazy__linearize_match.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_lazy/linearize_match.hvm
 ---
-λa λb switch a { 0: b; _: (+ a-1 b) }
+λa switch a = a { 0: λb b; _: λd (+ a-1 d) }
diff --git a/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap b/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap
index 0138d26a5..4e770fe47 100644
--- a/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap
+++ b/tests/snapshots/run_lazy__match_mult_linearization.hvm.snap
@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_lazy/match_mult_linearization.hvm
 ---
-λa switch a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) }
+λa switch a = a { 0: λb λc λd (+ (+ b c) d); _: λf λg λh (+ (+ (+ a-1 f) g) h) }
diff --git a/tests/snapshots/simplify_matches__adt_tup_era.hvm.snap b/tests/snapshots/simplify_matches__adt_tup_era.hvm.snap
index cf8af7ef1..e915ea864 100644
--- a/tests/snapshots/simplify_matches__adt_tup_era.hvm.snap
+++ b/tests/snapshots/simplify_matches__adt_tup_era.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/adt_tup_era.hvm
 ---
-(Foo) = λ%arg0 match %arg0 { Pair: match %arg0.a { Pair: %arg0.a.a } }
+(Foo) = λ%arg0 match %arg0 = %arg0 { Pair: match %arg0.a = %arg0.a { Pair: %arg0.a.a } }
 
 (Main) = (Foo (Pair 1 5))
 
diff --git a/tests/snapshots/simplify_matches__already_flat.hvm.snap b/tests/snapshots/simplify_matches__already_flat.hvm.snap
index d81a5f4b9..de81c8646 100644
--- a/tests/snapshots/simplify_matches__already_flat.hvm.snap
+++ b/tests/snapshots/simplify_matches__already_flat.hvm.snap
@@ -8,9 +8,9 @@ input_file: tests/golden_tests/simplify_matches/already_flat.hvm
 
 (Rule3) = λ%arg0 λ%arg1 λ%arg2 λ%arg3 (%arg0 %arg1 %arg2 %arg3)
 
-(Rule4) = λ%arg0 match %arg0 { CtrA: λx x; CtrB: %arg0.x }
+(Rule4) = λ%arg0 match %arg0 = %arg0 { CtrA: λx x; CtrB: %arg0.x }
 
-(Rule5) = λ%arg0 match %arg0 { CtrA1: λ%arg1 (%arg0.a %arg1); CtrA2: λ%arg1 (%arg0.a1 %arg0.a2 %arg1); CtrA3: λ%arg1 (match %arg1 { CtrB0: λ%arg0.a (CtrA3 %arg0.a); CtrB1: λ%arg0.a (CtrA3 %arg0.a %arg1.b); CtrB2: λ%arg0.a (CtrA3 %arg0.a (CtrB2 %arg1.b)); CtrB3: λ%arg0.a (%arg0.a %arg1.b) } %arg0.a) }
+(Rule5) = λ%arg0 match %arg0 = %arg0 { CtrA1: λ%arg1 (%arg0.a %arg1); CtrA2: λ%arg1 (%arg0.a1 %arg0.a2 %arg1); CtrA3: λ%arg1 (match %arg1 = %arg1 { CtrB0: λ%arg0.a (CtrA3 %arg0.a); CtrB1: λ%arg0.a (CtrA3 %arg0.a %arg1.b); CtrB2: λ%arg0.a (CtrA3 %arg0.a (CtrB2 %arg1.b)); CtrB3: λ%arg0.a (%arg0.a %arg1.b) } %arg0.a) }
 
 (Rule6) = λ%arg0 %arg0
 
diff --git a/tests/snapshots/simplify_matches__bits_dec.hvm.snap b/tests/snapshots/simplify_matches__bits_dec.hvm.snap
index abfa79274..1c9912a76 100644
--- a/tests/snapshots/simplify_matches__bits_dec.hvm.snap
+++ b/tests/snapshots/simplify_matches__bits_dec.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/bits_dec.hvm
 ---
-(Data.Bits.dec) = λ%arg0 match %arg0 { Data.Bits.e: Data.Bits.e; Data.Bits.o: match %arg0.t { Data.Bits.e: Data.Bits.e; Data.Bits.o: (Data.Bits.i (Data.Bits.dec %arg0.t.t)); Data.Bits.i: (Data.Bits.i (Data.Bits.dec %arg0.t.t)) }; Data.Bits.i: match %arg0.t { Data.Bits.e: (Data.Bits.o Data.Bits.e); Data.Bits.o: (Data.Bits.o %arg0.t.t); Data.Bits.i: (Data.Bits.o %arg0.t.t) } }
+(Data.Bits.dec) = λ%arg0 match %arg0 = %arg0 { Data.Bits.e: Data.Bits.e; Data.Bits.o: match %arg0.t = %arg0.t { Data.Bits.e: Data.Bits.e; Data.Bits.o: (Data.Bits.i (Data.Bits.dec %arg0.t.t)); Data.Bits.i: (Data.Bits.i (Data.Bits.dec %arg0.t.t)) }; Data.Bits.i: match %arg0.t = %arg0.t { Data.Bits.e: (Data.Bits.o Data.Bits.e); Data.Bits.o: (Data.Bits.o %arg0.t.t); Data.Bits.i: (Data.Bits.o %arg0.t.t) } }
 
 (Data.Bits.e) = #Data.Bits λData.Bits.e #Data.Bits λData.Bits.o #Data.Bits λData.Bits.i Data.Bits.e
 
diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap
index bcf37ec31..b34a11102 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/double_unwrap_box.hvm
 ---
-(DoubleUnbox) = λ%arg0 match %arg0 { Box: match %arg0.x { Box: λ%arg1 %arg0.x.x } }
+(DoubleUnbox) = λ%arg0 match %arg0 = %arg0 { Box: match %arg0.x = %arg0.x { Box: λ%arg1 %arg0.x.x } }
 
 (Main) = (DoubleUnbox (Box (Box 0)) 5)
 
diff --git a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
index 992cc2e9f..4218f0faf 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/double_unwrap_maybe.hvm
 ---
-(DoubleUnwrap) = λ%arg0 match %arg0 { Some: match %arg0.x { Some: λ%arg1 %arg0.x.x; None: λ%arg1 %arg1 }; None: λ%arg1 %arg1 }
+(DoubleUnwrap) = λ%arg0 match %arg0 = %arg0 { Some: match %arg0.x = %arg0.x { Some: λ%arg1 %arg0.x.x; None: λ%arg1 %arg1 }; None: λ%arg1 %arg1 }
 
 (Main) = (DoubleUnwrap (Some None) 5)
 
diff --git a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap
index 4fec93688..70e777bce 100644
--- a/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap
+++ b/tests/snapshots/simplify_matches__flatten_with_terminal.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/flatten_with_terminal.hvm
 ---
-(Foo) = λ%arg0 switch %arg0 { 0: λ%arg1 match %arg1 { A: match %arg1.b { B: B } }; _: λ%arg1 * }
+(Foo) = λ%arg0 switch %arg0 = %arg0 { 0: λ%arg1 match %arg1 = %arg1 { A: match %arg1.b = %arg1.b { B: B } }; _: λ%arg1 * }
 
 (main) = (Foo 2 (A B))
 
diff --git a/tests/snapshots/simplify_matches__linearize_match_all.hvm.snap b/tests/snapshots/simplify_matches__linearize_match_all.hvm.snap
index a30cc9e3e..4a2c793f2 100644
--- a/tests/snapshots/simplify_matches__linearize_match_all.hvm.snap
+++ b/tests/snapshots/simplify_matches__linearize_match_all.hvm.snap
@@ -2,23 +2,23 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/linearize_match_all.hvm
 ---
-(A) = λa switch a { 0: λb λc (b c); _: λb λc (a-1 b c) }
+(A) = λa switch a = a { 0: λb λc (b c); _: λb λc (a-1 b c) }
 
-(B) = λa λb λc (switch c { 0: λa λb (a b); _: λa λb (a b c-1) } a b)
+(B) = λa λb λc (switch c = c { 0: λa λb (a b); _: λa λb (a b c-1) } a b)
 
-(C) = λa λb λc switch c { 0: (a b); _: (a b c-1) }
+(C) = λa λb λc switch c = c { 0: (a b); _: (a b c-1) }
 
-(D) = λa switch a { 0: λb λc c; _: λb λc (a-1 c) }
+(D) = λa switch a = a { 0: λb λc c; _: λb λc (a-1 c) }
 
-(E) = λ%arg0 match %arg0 { Cons: λ%arg1 (match %arg1 { Cons: λ%arg0.h λ%arg0.t (%arg0.h %arg0.t %arg1.h %arg1.t); Nil: λ%arg0.h λ%arg0.t (Cons %arg0.h %arg0.t Nil) } %arg0.h %arg0.t); Nil: λ%arg1 (Nil %arg1) }
+(E) = λ%arg0 match %arg0 = %arg0 { Cons: λ%arg1 (match %arg1 = %arg1 { Cons: λ%arg0.h λ%arg0.t (%arg0.h %arg0.t %arg1.h %arg1.t); Nil: λ%arg0.h λ%arg0.t (Cons %arg0.h %arg0.t Nil) } %arg0.h %arg0.t); Nil: λ%arg1 (Nil %arg1) }
 
-(A2) = λa match a { Cons: λb λc (a.h a.t b c); Nil: λb λc (b c) }
+(A2) = λa match a = a { Cons: λb λc (a.h a.t b c); Nil: λb λc (b c) }
 
-(B2) = λa λb λc (match c { Cons: λa λb (a b c.h c.t); Nil: λa λb (a b) } a b)
+(B2) = λa λb λc (match c = c { Cons: λa λb (a b c.h c.t); Nil: λa λb (a b) } a b)
 
-(C2) = λa λb λc match c { Cons: (a b c.h c.t); Nil: (a b) }
+(C2) = λa λb λc match c = c { Cons: (a b c.h c.t); Nil: (a b) }
 
-(D2) = λa match a { Cons: λb λc (a.h a.t b c); Nil: λb λc (b c) }
+(D2) = λa match a = a { Cons: λb λc (a.h a.t b c); Nil: λb λc (b c) }
 
 (main) = *
 
diff --git a/tests/snapshots/simplify_matches__match_str.hvm.snap b/tests/snapshots/simplify_matches__match_str.hvm.snap
index d24852e0b..0009402c7 100644
--- a/tests/snapshots/simplify_matches__match_str.hvm.snap
+++ b/tests/snapshots/simplify_matches__match_str.hvm.snap
@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/match_str.hvm
 ---
-(is_as) = λ%arg0 match %arg0 { String.cons: let %arg0.head%matched = (- %arg0.head 65); (switch %arg0.head%matched { 0: λ%arg0.tail match %arg0.tail { String.cons: let %arg0.tail.head%matched = (- %arg0.tail.head 115); (switch %arg0.tail.head%matched { 0: λ%arg0.tail.tail match %arg0.tail.tail { String.cons: 0; String.nil: 2 }; _: λ%arg0.tail.tail 0 } %arg0.tail.tail); String.nil: 0 }; _: λ%arg0.tail let %arg0.head%matched = (- %arg0.head%matched-1 31); (switch %arg0.head%matched { 0: λ%arg0.tail match %arg0.tail { String.cons: let %arg0.tail.head%matched = (- %arg0.tail.head 115); (switch %arg0.tail.head%matched { 0: λ%arg0.tail.tail match %arg0.tail.tail { String.cons: 0; String.nil: 2 }; _: λ%arg0.tail.tail 0 } %arg0.tail.tail); String.nil: 0 }; _: λ%arg0.tail 0 } %arg0.tail) } %arg0.tail); String.nil: 1 }
+(is_as) = λ%arg0 match %arg0 = %arg0 { String.cons: (switch %arg0.head = (- %arg0.head 65) { 0: λ%arg0.tail match %arg0.tail = %arg0.tail { String.cons: (switch %arg0.tail.head = (- %arg0.tail.head 115) { 0: λ%arg0.tail.tail match %arg0.tail.tail = %arg0.tail.tail { String.cons: 0; String.nil: 2 }; _: λ%arg0.tail.tail 0 } %arg0.tail.tail); String.nil: 0 }; _: λ%arg0.tail (switch %arg0.head = (- %arg0.head-1 31) { 0: λ%arg0.tail match %arg0.tail = %arg0.tail { String.cons: (switch %arg0.tail.head = (- %arg0.tail.head 115) { 0: λ%arg0.tail.tail match %arg0.tail.tail = %arg0.tail.tail { String.cons: 0; String.nil: 2 }; _: λ%arg0.tail.tail 0 } %arg0.tail.tail); String.nil: 0 }; _: λ%arg0.tail 0 } %arg0.tail) } %arg0.tail); String.nil: 1 }
 
 (main) = *
diff --git a/tests/snapshots/simplify_matches__nested.hvm.snap b/tests/snapshots/simplify_matches__nested.hvm.snap
index f2f8977e7..e37a7940e 100644
--- a/tests/snapshots/simplify_matches__nested.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/nested.hvm
 ---
-(Rule) = λ%arg0 match %arg0 { CtrA: (match %arg0.b { CtrB1: λ%arg0.a (%arg0.a %arg0.b.b); CtrB2: λ%arg0.a (match %arg0.b.a { CtrC: λ%arg0.a λ%arg0.b.b (%arg0.a %arg0.b.b) } %arg0.a %arg0.b.b) } %arg0.a); CtrB: %arg0.a }
+(Rule) = λ%arg0 match %arg0 = %arg0 { CtrA: (match %arg0.b = %arg0.b { CtrB1: λ%arg0.a (%arg0.a %arg0.b.b); CtrB2: λ%arg0.a (match %arg0.b.a = %arg0.b.a { CtrC: λ%arg0.a λ%arg0.b.b (%arg0.a %arg0.b.b) } %arg0.a %arg0.b.b) } %arg0.a); CtrB: %arg0.a }
 
 (CtrA) = λa λb #Foo λCtrA #Foo λCtrB #Foo (CtrA a b)
 
diff --git a/tests/snapshots/simplify_matches__nested2.hvm.snap b/tests/snapshots/simplify_matches__nested2.hvm.snap
index a6e1410c8..b69b8233e 100644
--- a/tests/snapshots/simplify_matches__nested2.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested2.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/nested2.hvm
 ---
-(Foo) = λ%arg0 λ%arg1 (match %arg1 { List.cons: λ%arg0 (match %arg1.tail { List.cons: λ%arg0 λ%arg1.head (%arg0 %arg1.head %arg1.tail.head %arg1.tail.tail); List.nil: λ%arg0 λ%arg1.head (%arg0 (List.cons %arg1.head List.nil)) } %arg0 %arg1.head); List.nil: λ%arg0 (%arg0 List.nil) } %arg0)
+(Foo) = λ%arg0 λ%arg1 (match %arg1 = %arg1 { List.cons: λ%arg0 (match %arg1.tail = %arg1.tail { List.cons: λ%arg0 λ%arg1.head (%arg0 %arg1.head %arg1.tail.head %arg1.tail.tail); List.nil: λ%arg0 λ%arg1.head (%arg0 (List.cons %arg1.head List.nil)) } %arg0 %arg1.head); List.nil: λ%arg0 (%arg0 List.nil) } %arg0)
 
 (List.cons) = λhead λtail #List λList.cons #List λList.nil #List (List.cons head tail)
 
diff --git a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
index 29a716774..533941d86 100644
--- a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/nested_0ary.hvm
 ---
-(Unpack) = λ%arg0 λ%arg1 (match %arg1 { Cons: λ%arg0 (match %arg1.tail { Cons: λ%arg0 λ%arg1.head (%arg0 (Cons %arg1.head (Cons %arg1.tail.head %arg1.tail.tail))); Nil: λ%arg0 λ%arg1.head %arg1.head } %arg0 %arg1.head); Nil: λ%arg0 Nil } %arg0)
+(Unpack) = λ%arg0 λ%arg1 (match %arg1 = %arg1 { Cons: λ%arg0 (match %arg1.tail = %arg1.tail { Cons: λ%arg0 λ%arg1.head (%arg0 (Cons %arg1.head (Cons %arg1.tail.head %arg1.tail.tail))); Nil: λ%arg0 λ%arg1.head %arg1.head } %arg0 %arg1.head); Nil: λ%arg0 Nil } %arg0)
 
 (Cons) = λhead λtail #list λCons #list λNil #list (Cons head tail)
 
diff --git a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap
index eaead67ea..fe3d764e9 100644
--- a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap
+++ b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap
@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/redundant_with_era.hvm
 ---
-(Fn2) = λ%arg0 switch %arg0 { 0: λ%arg1 let (%arg1.0, %arg1.1) = %arg1; let (%arg1.1.0, %arg1.1.1) = %arg1.1; %arg1.1.1; _: λ%arg1 let (%arg1.0, %arg1.1) = %arg1; let (%arg1.1.0, %arg1.1.1) = %arg1.1; %arg1.1.1 }
+(Fn2) = λ%arg0 switch %arg0 = %arg0 { 0: λ%arg1 let (%arg1.0, %arg1.1) = %arg1; let (%arg1.1.0, %arg1.1.1) = %arg1.1; %arg1.1.1; _: λ%arg1 let (%arg1.0, %arg1.1) = %arg1; let (%arg1.1.0, %arg1.1.1) = %arg1.1; %arg1.1.1 }
 
 (main) = *