diff --git a/mat.hvmc b/mat.hvmc
deleted file mode 100644
index dac3bad2..00000000
--- a/mat.hvmc
+++ /dev/null
@@ -1 +0,0 @@
-@main = R & #2 ~ ?<#1 (a a) R>
\ No newline at end of file
diff --git a/src/lib.rs b/src/lib.rs
index b38219eb..d07e53f3 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,4 +1,12 @@
-#![feature(const_type_id, extern_types, inline_const, generic_const_exprs, new_uninit)]
+#![feature(
+  const_type_id,
+  extern_types,
+  inline_const,
+  generic_const_exprs,
+  new_uninit,
+  strict_overflow_ops,
+  iter_map_windows
+)]
 #![cfg_attr(feature = "trace", feature(const_type_name))]
 #![allow(non_snake_case, incomplete_features)]
 
diff --git a/src/main.rs b/src/main.rs
index f5f7b9e2..f7f26972 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -336,6 +336,9 @@ fn load_book(files: &[String], transform_opts: &TransformOpts) -> Book {
     );
   }
   for (_, def) in &mut book.nets {
+    if transform_passes.eta_reduce {
+      def.eta_reduce();
+    }
     for tree in def.trees_mut() {
       if transform_passes.coalesce_ctrs {
         tree.coalesce_constructors();
diff --git a/src/transform.rs b/src/transform.rs
index 460dd479..a79e85e9 100644
--- a/src/transform.rs
+++ b/src/transform.rs
@@ -1,3 +1,4 @@
 pub mod coalesce_ctrs;
 pub mod encode_adts;
+pub mod eta_reduce;
 pub mod pre_reduce;
diff --git a/src/transform/eta_reduce.rs b/src/transform/eta_reduce.rs
new file mode 100644
index 00000000..2a7f091d
--- /dev/null
+++ b/src/transform/eta_reduce.rs
@@ -0,0 +1,126 @@
+use std::collections::HashMap;
+
+use crate::ast::{Net, Tree};
+
+/// Converts (x y), (x y) into x, x
+impl Net {
+  pub fn eta_reduce(&mut self) {
+    let mut phase1 = Phase1::default();
+    phase1.walk_and_sort_net(self);
+    println!("{:?}", phase1.gaps);
+    let mut phase2 = Phase2 { gaps: phase1.gaps };
+    phase2.reduce_net(self);
+  }
+}
+
+#[derive(Debug)]
+enum NodeType {
+  Var(isize),
+  Ctr(u16),
+  Other,
+  Hole,
+}
+
+#[derive(Default)]
+struct Phase1<'a> {
+  vars: HashMap<&'a str, usize>,
+  gaps: Vec<NodeType>,
+}
+
+impl<'a> Phase1<'a> {
+  fn walk_and_sort_net(&mut self, net: &'a mut Net) {
+    self.walk_and_sort_tree(&mut net.root);
+    for (a, b) in net.redexes.iter_mut() {
+      self.walk_and_sort_tree(a);
+      self.walk_and_sort_tree(b);
+    }
+  }
+  fn walk_and_sort_tree(&mut self, tree: &'a mut Tree) {
+    match tree {
+      Tree::Ctr { lab, ports } => {
+        let last_port = ports.len() - 1;
+        for (idx, i) in ports.iter_mut().enumerate() {
+          if idx != last_port {
+            self.gaps.push(NodeType::Ctr(*lab));
+          }
+          self.walk_and_sort_tree(i);
+        }
+      }
+      Tree::Var { nam } => {
+        let nam: &str = &*nam;
+        if let Some(i) = self.vars.get(nam) {
+          let j = self.gaps.len() as isize;
+          self.gaps.push(NodeType::Var(*i as isize - j));
+          self.gaps[*i] = NodeType::Var(j - *i as isize);
+        } else {
+          self.vars.insert(nam, self.gaps.len());
+          self.gaps.push(NodeType::Hole);
+        }
+      }
+      _ => {
+        self.gaps.push(NodeType::Other);
+        for i in tree.children_mut() {
+          self.walk_and_sort_tree(i);
+        }
+      }
+    }
+  }
+}
+
+struct Phase2 {
+  gaps: Vec<NodeType>,
+}
+
+impl Phase2 {
+  fn reduce_net(&mut self, net: &mut Net) {
+    let mut index = 0;
+    self.reduce_tree(&mut net.root, &mut index);
+    for (a, b) in net.redexes.iter_mut() {
+      self.reduce_tree(a, &mut index);
+      self.reduce_tree(b, &mut index);
+    }
+  }
+  fn reduce_tree(&mut self, tree: &mut Tree, index: &mut usize) {
+    match tree {
+      ctr @ Tree::Ctr { .. } => {
+        let Tree::Ctr { lab, ports } = ctr else { unreachable!() };
+        // reduce from the inside of the n-ary node to the outside
+        let mut indices = vec![];
+        let last_port = ports.len() - 1;
+        for (idx, i) in ports.iter_mut().enumerate() {
+          indices.push(*index);
+          if idx != last_port {
+            *index += 1;
+          }
+          self.reduce_tree(i, index);
+        }
+        while indices.len() > 1 {
+          let tail_var = indices.pop().unwrap();
+          let head_ctr = indices.pop().unwrap();
+          let head_var = head_ctr + 1;
+          if let (NodeType::Var(off1), NodeType::Var(off2)) = (&self.gaps[head_var], &self.gaps[tail_var]) {
+            if off1 == off2 {
+              if let NodeType::Ctr(other_lab) = &self.gaps[head_ctr.strict_add_signed(*off1)] {
+                if other_lab == lab {
+                  indices.push(head_var);
+                  ports.pop();
+                  continue;
+                }
+              }
+            }
+          }
+          break;
+        }
+        if ports.len() == 1 {
+          *ctr = ports.pop().unwrap();
+        }
+      }
+      tree => {
+        *index += 1;
+        for i in tree.children_mut() {
+          self.reduce_tree(i, index);
+        }
+      }
+    }
+  }
+}
diff --git a/test.hvm b/test.hvm
deleted file mode 100644
index d4fef356..00000000
--- a/test.hvm
+++ /dev/null
@@ -1,142 +0,0 @@
-// Interaction Calculus of Constructions
-// =====================================
-
-// Type
-// ----
-
-data Term
-  = (Lam bod)
-  | (App fun arg)
-  | (Val bod)
-  | (Ann val typ)
-  | (Var idx)
-  | (Err term)
-
-// Evaluation
-// ----------
-
-(APP fun arg) = match fun {
-  Lam: (fun.bod arg)
-  Val: (Val λx(APP (fun.bod (Lam λ$k(x))) (ANN $k arg)))
-  Err: (App (Err fun.term) arg)
-  var: (App var arg)
-}
-
-// Compares two reduced types
-(Equal (Var i1) (Var i2)) = (== i1 i2)
-(Equal (App f1 a1) (App f2 a2)) = (& (Equal f1 f2) (Equal a1 a2))
-(Equal t1 t2) = 0
-
-// Checks if a term can be an instance of a reduced type.
-(Check (Var i) (Var j)) = match k = (== i j) {
-  0: (Ann (Var i) (Var j))
-  1+: (Err (Ann (Var i) (Var j)))
-}
-(Check (Ann val t1) t2) = match k = (Equal t1 t2) {
-  0: (Err (Ann (Ann val t1) t2))
-  1+: (Check val t1)
-}
-(Check (App val t1) (Var j)) = (Ann (App val t1) (Var j))
-(Check val typ) = (Err (Ann val typ))
-
-(ANN val typ) = match typ {
-  Lam: (Lam λx(ANN (APP val $k) (typ.bod (Val λ$k(x)))))
-  Val: (typ.bod val)
-  Err: (Ann val (Err typ.term))
-  var: (Check val var)
-}
-
-// Equality
-// --------
-
-// TODO!
-
-// Encodings
-// ---------
-
-// (A -> B) ::= θv λx {(v {x: A}): B}
-(Arr A B) = (Val λv(Lam λx(ANN (APP v (ANN x A)) B)))
-
-// (Π(x: A). B[x]) ::= θv λx {(v {x: A}): (B x)}
-(All A B) = (Val λv(Lam λx(ANN (APP v (ANN x A)) (B x))))
-
-// Stringification
-// ---------------
-
-(Concat String.nil         ys) = ys
-(Concat (String.cons x xs) ys) = (String.cons x (Concat xs ys))
-
-(Join List.nil)         = ""
-(Join (List.cons x xs)) = (Concat x (Join xs))
-
-(U60.show n) = (U60.show.go n String.nil)
-(U60.show.go n res) = match k = (< n 10) {
-  0: (U60.show.go (/ n 10) (String.cons (+ '0' (% n 10)) res))
-  1+: (String.cons (+ '0' n) res)
-}
-
-(Show term dep) = match term {
-  Lam: (Join ["λx" (U60.show dep) " " (Show (term.bod (Var dep)) (+ dep 1))])
-  App: (Join ["(" (Show term.fun dep) " " (Show term.arg dep) ")"])
-  Val: (Join ["θx" (U60.show dep) " " (Show (term.bod (Var dep)) (+ dep 1))])
-  Ann: (Join ["{" (Show term.val dep) " : " (Show term.typ dep) "}"])
-  Var: (Join ["x" (U60.show term.idx)])
-  Err: (Join ["Err[" (Show term.term dep) "]"])
-}
-
-LF = (String.cons 10 String.nil) 
-
-(CheckShow term type) = (Join [
-  "Checking: " (Show (Ann term type) 0) LF
-  "Result: " (Show (ANN term type) 0) LF
-])
-
-// Tests
-// -----
-
-Main =
-  let Set = (Var (- 0 1))
-  let Any = (Val λx(x))
-
-  let id = (Lam λx x)
-
-  //  Bool = ∀(P: *) ∀(t: P) ∀(f: P) P
-  let Bool = (All Any λp (All p λt (All p λf(p))))
-
-  // Eq (T: Type) (a: T) (b: T) : Type = (P: T -> Type) (h: P a) -> P b
-  let Eq = (Lam λT (All T λa (All T λb(All (Arr T Any) λP(Arr (P a) (P b))))))
-  let refl = (Lam λT (Lam λa (Lam λb (Lam λP(Lam λh h)))))
-
-  let Empty = (All Any λp p)
-
-  //  true = λP λt λf t
-  let true = (Lam λP(Lam λt(Lam λf(t))))
-
-  //  false = λP λt λf f
-  let false = (Lam λP(Lam λt(Lam λf(f))))
-
-  //  Test : ∀(A: *) ∀(B: *) ∀(A -> B) ∀(B -> A) ∀A A
-  //       = λA λB λab λba λa a
-  let TEST = (All Any λA(All Any λB(Arr (Arr A B) (Arr (Arr B A) (Arr A B)))))
-  let test = (Lam λA(Lam λB(Lam λab(Lam λba(Lam λa(APP ab a)))))) 
-
-  // doesn't work :(
-  let funext = (CheckShow
-    (Lam λT(Lam λU(Lam λf(Lam λg(Lam λh(Lam λP(Lam λa
-      (APP (APP (APP h $t) (All U λu(APP P (All T λ$t(u))))) a)
-    )))))))
-    (All Any λT(All Any λU(All (Arr T U) λf(All (Arr T U) λg(
-      All (All T λt (APP (APP (APP Eq U) (APP f t)) (APP g t))) λh
-      (APP (APP (APP Eq (Arr T U)) f) g)
-    )))))
-  )
-
- (Join [
-    (CheckShow (Lam λA(Lam λB(Lam λab(Lam λba(Lam λa(APP ab a)))))) (All Any λA(All Any λB(Arr (Arr A B) (Arr (Arr B A) (Arr A B))))))
-    (CheckShow (Lam λA(Lam λB(Lam λab(Lam λba(Lam λa(APP ab a)))))) (All Any λA(All Any λB(Arr (Arr A B) (Arr (Arr B A) (Arr A A))))))
-    (CheckShow (Lam λA(Lam λB(Lam λab(Lam λba(Lam λa a))))) (All Any λA(All Any λB(Arr (Arr A B) (Arr (Arr B A) (Arr A A))))))
-    (CheckShow (Lam λx x) (All Any λP P))
-    (CheckShow (Lam λx (APP x Bool)) (Arr (All Any λP P) Bool))
-    (CheckShow true Bool)
-    (CheckShow (APP refl Bool) (APP Eq Bool))
-  ])
diff --git a/test.hvmc b/test.hvmc
deleted file mode 100644
index 0d4d0772..00000000
--- a/test.hvmc
+++ /dev/null
@@ -1,390 +0,0 @@
-@ANN = (a ({2 @ANN$S0 {2 @ANN$S1 {2 @ANN$S2 {2 @ANN$S3 {2 @ANN$S4 {2 @ANN$S5 (a b)}}}}}} b))
-@ANN$S0 = {2 (a b) (c d)}
-& @Lam ~ ((e f) d)
-& @ANN ~ (g (b f))
-& @APP ~ (c (h g))
-& @Val ~ ((h e) a)
-@ANN$S1 = {2 a {2 b (c d)}}
-& @Check ~ (c (e d))
-& @App ~ (a (b e))
-@ANN$S2 = {2 (a b) (a b)}
-@ANN$S3 = {2 a {2 b (c d)}}
-& @Check ~ (c (e d))
-& @Ann ~ (a (b e))
-@ANN$S4 = {2 a (b c)}
-& @Check ~ (b (d c))
-& @Var ~ (a d)
-@ANN$S5 = {2 a (b c)}
-& @Ann ~ (b (d c))
-& @Err ~ (a d)
-@APP = ({2 @APP$S0 {2 @APP$S1 {2 @APP$S2 {2 @APP$S3 {2 @APP$S4 {2 @APP$S5 (a b)}}}}}} (a b))
-@APP$S0 = {2 (a b) (a b)}
-@APP$S1 = {2 a {2 b (c d)}}
-& @App ~ (e (c d))
-& @App ~ (a (b e))
-@APP$S2 = {2 (a b) (c d)}
-& @Val ~ ((e f) d)
-& @APP ~ (b (g f))
-& @ANN ~ (h (c g))
-& @Lam ~ ((h e) a)
-@APP$S3 = {2 a {2 b (c d)}}
-& @App ~ (e (c d))
-& @Ann ~ (a (b e))
-@APP$S4 = {2 a (b c)}
-& @App ~ (d (b c))
-& @Var ~ (a d)
-@APP$S5 = {2 a (b c)}
-& @App ~ (d (b c))
-& @Err ~ (a d)
-@All = (a ((b c) d))
-& @Val ~ ((e f) d)
-& @Lam ~ (({3 g b} h) f)
-& @ANN ~ (i (c h))
-& @APP ~ (e (j i))
-& @ANN ~ (g (a j))
-@Ann = (a (b {2 * {2 * {2 * {2 {2 a {2 b c}} {2 * {2 * c}}}}}}))
-@App = (a (b {2 * {2 {2 a {2 b c}} {2 * {2 * {2 * {2 * c}}}}}}))
-@Arr = (a (b c))
-& @Val ~ ((d e) c)
-& @Lam ~ ((f g) e)
-& @ANN ~ (h (b g))
-& @APP ~ (d (i h))
-& @ANN ~ (f (a i))
-@Check = ({2 @Check$S0 {2 @Check$S7 {2 @Check$S8 {2 @Check$S12 {2 @Check$S22 {2 @Check$S23 (a b)}}}}}} (a b))
-@Check$S0 = {2 a (b c)}
-& @Err ~ (d c)
-& @Ann ~ (e (b d))
-& @Lam ~ (a e)
-@Check$S1 = {2 a (b (c d))}
-& @Err ~ (e d)
-& @Ann ~ (f (g e))
-& @Lam ~ (a g)
-& @App ~ (c (b f))
-@Check$S10 = (a (* (b c)))
-& @Check ~ (b (a c))
-@Check$S12 = {2 a {2 {35 b c} ({33 d e} f)}}
-& @Equal ~ (c (e ?<(@Check$S9 (* @Check$S10)) (b (d (a f)))>))
-@Check$S13 = {2 a (b c)}
-& @Err ~ (d c)
-& @Ann ~ (e (f d))
-& @Lam ~ (a f)
-& @Var ~ (b e)
-@Check$S14 = {2 a {2 b (c d)}}
-& @Err ~ (e d)
-& @Ann ~ (f (g e))
-& @App ~ (a (b g))
-& @Var ~ (c f)
-@Check$S15 = {2 a (b c)}
-& @Err ~ (d c)
-& @Ann ~ (e (f d))
-& @Val ~ (a f)
-& @Var ~ (b e)
-@Check$S16 = {2 a {2 b (c d)}}
-& @Err ~ (e d)
-& @Ann ~ (f (g e))
-& @Ann ~ (a (b g))
-& @Var ~ (c f)
-@Check$S17 = (a (b c))
-& @Ann ~ (d (e c))
-& @Var ~ (b e)
-& @Var ~ (a d)
-@Check$S18 = (a (b c))
-& @Err ~ (d c)
-& @Ann ~ (e (f d))
-& @Var ~ (b f)
-& @Var ~ (a e)
-@Check$S2 = {2 a {2 b (c (d e))}}
-& @Err ~ (f e)
-& @Ann ~ (g (h f))
-& @App ~ (a (b h))
-& @App ~ (d (c g))
-@Check$S20 = {2 {37 a b} ({39 c <== b ?<(@Check$S17 (* @Check$S18)) (c (a d))>>} d)}
-@Check$S21 = {2 a (b c)}
-& @Err ~ (d c)
-& @Ann ~ (e (f d))
-& @Err ~ (a f)
-& @Var ~ (b e)
-@Check$S22 = {2 a ({2 @Check$S13 {2 @Check$S14 {2 @Check$S15 {2 @Check$S16 {2 @Check$S20 {2 @Check$S21 (a b)}}}}}} b)}
-@Check$S23 = {2 a (b c)}
-& @Err ~ (d c)
-& @Ann ~ (e (b d))
-& @Err ~ (a e)
-@Check$S3 = {2 a (b (c d))}
-& @Err ~ (e d)
-& @Ann ~ (f (g e))
-& @Val ~ (a g)
-& @App ~ (c (b f))
-@Check$S4 = {2 a {2 b (c (d e))}}
-& @Err ~ (f e)
-& @Ann ~ (g (h f))
-& @Ann ~ (a (b h))
-& @App ~ (d (c g))
-@Check$S5 = {2 a (b (c d))}
-& @Ann ~ (e (f d))
-& @Var ~ (a f)
-& @App ~ (c (b e))
-@Check$S6 = {2 a (b (c d))}
-& @Err ~ (e d)
-& @Ann ~ (f (g e))
-& @Err ~ (a g)
-& @App ~ (c (b f))
-@Check$S7 = {2 a {2 b ({2 @Check$S1 {2 @Check$S2 {2 @Check$S3 {2 @Check$S4 {2 @Check$S5 {2 @Check$S6 (b (a c))}}}}}} c)}}
-@Check$S8 = {2 a (b c)}
-& @Err ~ (d c)
-& @Ann ~ (e (b d))
-& @Val ~ (a e)
-@Check$S9 = (a (b (c d)))
-& @Err ~ (e d)
-& @Ann ~ (f (b e))
-& @Ann ~ (c (a f))
-@CheckShow = ({9 a b} ({7 c d} e))
-& @Join ~ (f e)
-& @List.cons ~ (g (h f))
-& @List.cons ~ (i (j h))
-& @List.cons ~ (@LF (k j))
-& @List.cons ~ (l (m k))
-& @List.cons ~ (n (o m))
-& @List.cons ~ (@LF (@List.nil o))
-& @Show ~ (p (#0 n))
-& @ANN ~ (b (d p))
-& @String.cons ~ (#82 (q l))
-& @String.cons ~ (#101 (r q))
-& @String.cons ~ (#115 (s r))
-& @String.cons ~ (#117 (t s))
-& @String.cons ~ (#108 (u t))
-& @String.cons ~ (#116 (v u))
-& @String.cons ~ (#58 (w v))
-& @String.cons ~ (#32 (@String.nil w))
-& @Show ~ (x (#0 i))
-& @Ann ~ (a (c x))
-& @String.cons ~ (#67 (y g))
-& @String.cons ~ (#104 (z y))
-& @String.cons ~ (#101 (ab z))
-& @String.cons ~ (#99 (bb ab))
-& @String.cons ~ (#107 (cb bb))
-& @String.cons ~ (#105 (db cb))
-& @String.cons ~ (#110 (eb db))
-& @String.cons ~ (#103 (fb eb))
-& @String.cons ~ (#58 (gb fb))
-& @String.cons ~ (#32 (@String.nil gb))
-@Concat = ({4 @Concat$S0 {4 (a a) (b c)}} (b c))
-@Concat$S0 = {4 a {4 b (c d)}}
-& @String.cons ~ (a (e d))
-& @Concat ~ (b (c e))
-@Equal = ({2 @Equal$S1 {2 @Equal$S19 {2 @Equal$S21 {2 @Equal$S24 {2 @Equal$S38 {2 @Equal$S40 (a b)}}}}}} (a b))
-@Equal$S0 = (* #0)
-@Equal$S1 = {2 * @Equal$S0}
-@Equal$S10 = (* @Equal$S9)
-@Equal$S11 = {2 * @Equal$S10}
-@Equal$S12 = {2 * @Equal$S11}
-@Equal$S13 = (* #0)
-@Equal$S14 = (* @Equal$S13)
-@Equal$S15 = {2 * @Equal$S14}
-@Equal$S16 = (* #0)
-@Equal$S17 = (* @Equal$S16)
-@Equal$S18 = {2 * @Equal$S17}
-@Equal$S19 = {2 a {2 b ({2 @Equal$S4 {2 @Equal$S5 {2 @Equal$S8 {2 @Equal$S12 {2 @Equal$S15 {2 @Equal$S18 (b (a c))}}}}}} c)}}
-@Equal$S2 = (* #0)
-@Equal$S20 = (* #0)
-@Equal$S21 = {2 * @Equal$S20}
-@Equal$S22 = (* #0)
-@Equal$S23 = {2 * @Equal$S22}
-@Equal$S24 = {2 * @Equal$S23}
-@Equal$S25 = (* #0)
-@Equal$S26 = {2 * @Equal$S25}
-@Equal$S27 = (* #0)
-@Equal$S28 = {2 * @Equal$S27}
-@Equal$S29 = {2 * @Equal$S28}
-@Equal$S3 = (* @Equal$S2)
-@Equal$S30 = (* #0)
-@Equal$S31 = {2 * @Equal$S30}
-@Equal$S32 = (* #0)
-@Equal$S33 = {2 * @Equal$S32}
-@Equal$S34 = {2 * @Equal$S33}
-@Equal$S35 = {2 a (<== a b> b)}
-@Equal$S36 = (* #0)
-@Equal$S37 = {2 * @Equal$S36}
-@Equal$S38 = {2 a ({2 @Equal$S26 {2 @Equal$S29 {2 @Equal$S31 {2 @Equal$S34 {2 @Equal$S35 {2 @Equal$S37 (a b)}}}}}} b)}
-@Equal$S39 = (* #0)
-@Equal$S4 = {2 * @Equal$S3}
-@Equal$S40 = {2 * @Equal$S39}
-@Equal$S5 = {2 a {2 b (c (d e))}}
-& @Equal ~ (d (a <& f e>))
-& @Equal ~ (c (b f))
-@Equal$S6 = (* #0)
-@Equal$S7 = (* @Equal$S6)
-@Equal$S8 = {2 * @Equal$S7}
-@Equal$S9 = (* #0)
-@Err = (a {2 * {2 * {2 * {2 * {2 * {2 {2 a b} b}}}}}})
-@Join = ({6 @Join$S0 {6 @String.nil a}} a)
-@Join$S0 = {6 a {6 b c}}
-& @Concat ~ (a (d c))
-& @Join ~ (b d)
-@LF = a
-& @String.cons ~ (#10 (@String.nil a))
-@Lam = (a {2 {2 a b} {2 * {2 * {2 * {2 * {2 * b}}}}}})
-@List.cons = (a (b {6 {6 a {6 b c}} {6 * c}}))
-@List.nil = {6 * {6 a a}}
-@Show = ({2 @Show$S0 {2 @Show$S1 {2 @Show$S2 {2 @Show$S3 {2 @Show$S4 {2 @Show$S5 (a b)}}}}}} (a b))
-@Show$S0 = {2 (a b) ({41 c {41 d <+ #1 e>}} f)}
-& @Join ~ (g f)
-& @List.cons ~ (h (i g))
-& @List.cons ~ (j (k i))
-& @List.cons ~ (l (m k))
-& @List.cons ~ (n (@List.nil m))
-& @Show ~ (b (e n))
-& @String.cons ~ (#32 (@String.nil l))
-& @U60.show ~ (c j)
-& @String.cons ~ (#955 (o h))
-& @String.cons ~ (#120 (@String.nil o))
-& @Var ~ (d a)
-@Show$S1 = {2 a {2 b ({43 c d} e)}}
-& @Join ~ (f e)
-& @List.cons ~ (g (h f))
-& @List.cons ~ (i (j h))
-& @List.cons ~ (k (l j))
-& @List.cons ~ (m (n l))
-& @List.cons ~ (o (@List.nil n))
-& @String.cons ~ (#41 (@String.nil o))
-& @Show ~ (b (d m))
-& @String.cons ~ (#32 (@String.nil k))
-& @Show ~ (a (c i))
-& @String.cons ~ (#40 (@String.nil g))
-@Show$S2 = {2 (a b) ({45 c {45 d <+ #1 e>}} f)}
-& @Join ~ (g f)
-& @List.cons ~ (h (i g))
-& @List.cons ~ (j (k i))
-& @List.cons ~ (l (m k))
-& @List.cons ~ (n (@List.nil m))
-& @Show ~ (b (e n))
-& @String.cons ~ (#32 (@String.nil l))
-& @U60.show ~ (c j)
-& @String.cons ~ (#952 (o h))
-& @String.cons ~ (#120 (@String.nil o))
-& @Var ~ (d a)
-@Show$S3 = {2 a {2 b ({47 c d} e)}}
-& @Join ~ (f e)
-& @List.cons ~ (g (h f))
-& @List.cons ~ (i (j h))
-& @List.cons ~ (k (l j))
-& @List.cons ~ (m (n l))
-& @List.cons ~ (o (@List.nil n))
-& @String.cons ~ (#125 (@String.nil o))
-& @Show ~ (b (d m))
-& @String.cons ~ (#32 (p k))
-& @String.cons ~ (#58 (q p))
-& @String.cons ~ (#32 (@String.nil q))
-& @Show ~ (a (c i))
-& @String.cons ~ (#123 (@String.nil g))
-@Show$S4 = {2 a (* b)}
-& @Join ~ (c b)
-& @List.cons ~ (d (e c))
-& @List.cons ~ (f (@List.nil e))
-& @U60.show ~ (a f)
-& @String.cons ~ (#120 (@String.nil d))
-@Show$S5 = {2 a (b c)}
-& @Join ~ (d c)
-& @List.cons ~ (e (f d))
-& @List.cons ~ (g (h f))
-& @List.cons ~ (i (@List.nil h))
-& @String.cons ~ (#93 (@String.nil i))
-& @Show ~ (a (b g))
-& @String.cons ~ (#69 (j e))
-& @String.cons ~ (#114 (k j))
-& @String.cons ~ (#114 (l k))
-& @String.cons ~ (#91 (@String.nil l))
-@String.cons = (a (b {4 {4 a {4 b c}} {4 * c}}))
-@String.nil = {4 * {4 a a}}
-@U60.show = (a b)
-& @U60.show.go ~ (a (@String.nil b))
-@U60.show.go = ({5 a << #10 ?<(@U60.show.go$S0 (* @U60.show.go$S1)) (a (b c))>>} (b c))
-@U60.show.go$S0 = ({49 </ #10 a> <% #10 b>} (c d))
-& @U60.show.go ~ (a (e d))
-& @String.cons ~ (f (c e))
-& #48 ~ <+ b f>
-@U60.show.go$S1 = (a (b c))
-& @String.cons ~ (d (b c))
-& #48 ~ <+ a d>
-@Val = (a {2 * {2 * {2 {2 a b} {2 * {2 * {2 * b}}}}}})
-@Var = (a {2 * {2 * {2 * {2 * {2 {2 a b} {2 * b}}}}}})
-@main = a
-& @Join ~ (b a)
-& @List.cons ~ (c (d b))
-& @List.cons ~ (e (f d))
-& @List.cons ~ (g (h f))
-& @List.cons ~ (i (j h))
-& @List.cons ~ (k (l j))
-& @List.cons ~ (m (n l))
-& @List.cons ~ (o (@List.nil n))
-& @CheckShow ~ (p (q o))
-& @APP ~ (r (s q))
-& @All ~ (t (({15 u {15 v w}} x) {13 y {13 z {13 ab {13 bb s}}}}))
-& @APP ~ (cb (bb p))
-& @Lam ~ ((* db) cb)
-& @Lam ~ ((* eb) db)
-& @Lam ~ ((* fb) eb)
-& @Lam ~ ((* gb) fb)
-& @Lam ~ ((hb hb) gb)
-& @CheckShow ~ (ib (ab m))
-& @Lam ~ ((* jb) ib)
-& @Lam ~ ((kb lb) jb)
-& @Lam ~ ((* kb) lb)
-& @Arr ~ (mb (z nb))
-& @CheckShow ~ (ob (nb k))
-& @Lam ~ ((pb qb) ob)
-& @APP ~ (pb (y qb))
-& @All ~ (rb ((sb sb) mb))
-& @Val ~ ((tb tb) {11 ub {11 vb {11 wb {11 xb {11 yb {11 zb {11 ac {11 rb {11 bc t}}}}}}}}})
-& @Arr ~ (cc (bc dc))
-& @All ~ (dc (({31 (ec fc) (gc hc)} ic) jc))
-& @All ~ (kc ((gc jc) lc))
-& @All ~ (mc ((ec lc) nc))
-& @Lam ~ (({29 mc {29 kc cc}} nc) r)
-& @Arr ~ (fc (hc ic))
-& @All ~ (ac ((oc oc) pc))
-& @CheckShow ~ (qc (pc i))
-& @Lam ~ ((rc rc) qc)
-& @All ~ (zb (({27 sc tc} uc) vc))
-& @All ~ (yb (({25 wc {25 xc {25 yc zc}}} vc) ad))
-& @CheckShow ~ (bd (ad g))
-& @Lam ~ ((* cd) bd)
-& @Lam ~ ((* dd) cd)
-& @Lam ~ ((* ed) dd)
-& @Lam ~ ((* fd) ed)
-& @Lam ~ ((gd gd) fd)
-& @Arr ~ (yc (zc hd))
-& @Arr ~ (id (hd jd))
-& @Arr ~ (kd (jd uc))
-& @Arr ~ (wc (sc kd))
-& @Arr ~ (tc (xc id))
-& @All ~ (xb (({23 ld md} nd) od))
-& @All ~ (wb (({21 pd {21 qd {21 rd sd}}} od) td))
-& @CheckShow ~ (ud (td e))
-& @Lam ~ ((* vd) ud)
-& @Lam ~ ((* wd) vd)
-& @Lam ~ ((xd yd) wd)
-& @Lam ~ ((* zd) yd)
-& @Lam ~ ((ae be) zd)
-& @APP ~ (xd (ae be))
-& @Arr ~ (rd (sd ce))
-& @Arr ~ (de (ce ee))
-& @Arr ~ (fe (ee nd))
-& @Arr ~ (pd (ld fe))
-& @Arr ~ (md (qd de))
-& @All ~ (vb (({19 ge {19 he ie}} je) ke))
-& @All ~ (ub (({17 le {17 me ne}} ke) oe))
-& @CheckShow ~ (pe (oe c))
-& @Lam ~ ((* qe) pe)
-& @Lam ~ ((* re) qe)
-& @Lam ~ ((se te) re)
-& @Lam ~ ((* ue) te)
-& @Lam ~ ((ve we) ue)
-& @APP ~ (se (ve we))
-& @Arr ~ (ne (ie xe))
-& @Arr ~ (ye (xe ze))
-& @Arr ~ (af (ze je))
-& @Arr ~ (le (ge af))
-& @Arr ~ (he (me ye))
-& @All ~ (u ((* bf) x))
-& @All ~ (v ((* w) bf))
-
diff --git a/tests/transform.rs b/tests/transform.rs
index d4014992..b81aeeec 100644
--- a/tests/transform.rs
+++ b/tests/transform.rs
@@ -43,9 +43,7 @@ pub fn test_adt_encoding() {
   use std::str::FromStr;
   pub fn parse_and_encode(net: &str) -> String {
     let mut net = Net::from_str(net).unwrap();
-    println!("{net}");
     net.trees_mut().for_each(Tree::coalesce_constructors);
-    println!("{net}");
     net.trees_mut().for_each(Tree::encode_scott_adts);
     format!("{net}")
   }
@@ -63,3 +61,21 @@ pub fn test_adt_encoding() {
   assert_display_snapshot!(parse_and_encode("(* ((a (b (c R))) R))"), @"(:1:2 a b c)");
   assert_display_snapshot!(parse_and_encode("{4 * {4 {4 a {4 b {4 c R}}} R}}"), @"{4:1:2 a b c}");
 }
+
+#[test]
+pub fn test_eta() {
+  use hvmc::ast::Net;
+  use std::str::FromStr;
+  pub fn parse_and_reduce(net: &str) -> String {
+    let mut net = Net::from_str(net).unwrap();
+    net.eta_reduce();
+    format!("{net}")
+  }
+  assert_display_snapshot!(parse_and_reduce("((x y) (x y))"), @"(x x)");
+  assert_display_snapshot!(parse_and_reduce("((a b c d e f) (a b c d e f))"), @"(a a)");
+  assert_display_snapshot!(parse_and_reduce("<+ (a b) (a b)>"), @"<+ a a>");
+  assert_display_snapshot!(parse_and_reduce("(a b) & ((a b) (c d)) ~ (c d) "), @r###"
+  a
+  & (a c) ~ c
+  "###);
+}