diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 23f23d62c2..d6d0bcc543 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -55,6 +55,41 @@ let evaluate_extend_env_with_pat =
 
 let alpha_magic = "__alpha_id__";
 
+let tangle =
+    (
+      dp: DHPat.t,
+      denv: ClosureEnvironment.t,
+      fp: DHPat.t,
+      fenv: ClosureEnvironment.t,
+    )
+    : option((ClosureEnvironment.t, ClosureEnvironment.t)) => {
+  let dvars = DHPat.bound_vars(dp);
+  let fvars = DHPat.bound_vars(fp);
+  if (List.length(dvars) != List.length(fvars)) {
+    None;
+  } else {
+    let ids =
+      Array.init(List.length(dvars), _ => {
+        alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4))
+      });
+    let denv_subst: list((string, 'a)) =
+      List.mapi(
+        (i, binding) =>
+          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+        dvars,
+      );
+    let fenv_subst: list((string, 'a)) =
+      List.mapi(
+        (i, binding) =>
+          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+        fvars,
+      );
+    let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv);
+    let fenv = evaluate_extend_env(Environment.of_list(fenv_subst), fenv);
+    Some((denv, fenv));
+  };
+};
+
 let rec matches_exp =
         (
           ~denv: ClosureEnvironment.t,
@@ -76,34 +111,26 @@ let rec matches_exp =
     | (Constructor("$v", _), _) => failwith("$v in matched expression")
 
     // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps
-    | (FixF(dp, dc, _), FixF(fp, fc, _)) =>
-      let dvars = DHPat.bound_vars(dp);
-      let fvars = DHPat.bound_vars(fp);
-      if (List.length(dvars) != List.length(fvars)) {
-        false;
-      } else {
-        let ids =
-          Array.init(List.length(dvars), _ => {
-            alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4))
-          });
-        let denv_subst: list((string, 'a)) =
-          List.mapi(
-            (i, binding) =>
-              (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
-            dvars,
-          );
-        let fenv_subst: list((string, 'a)) =
-          List.mapi(
-            (i, binding) =>
-              (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
-            fvars,
-          );
-        let denv =
-          evaluate_extend_env(Environment.of_list(denv_subst), denv);
-        let fenv =
-          evaluate_extend_env(Environment.of_list(fenv_subst), fenv);
-        matches_exp(~denv, dc, ~fenv, fc);
-      };
+    | (FixF(dp, dc, None), FixF(fp, fc, None)) =>
+      switch (tangle(dp, denv, fp, fenv)) {
+      | None => false
+      | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc)
+      }
+    | (FixF(dp, dc, None), FixF(fp, fc, Some(fenv))) =>
+      switch (tangle(dp, denv, fp, fenv)) {
+      | None => false
+      | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc)
+      }
+    | (FixF(dp, dc, Some(denv)), FixF(fp, fc, None)) =>
+      switch (tangle(dp, denv, fp, fenv)) {
+      | None => false
+      | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc)
+      }
+    | (FixF(dp, dc, Some(denv)), FixF(fp, fc, Some(fenv))) =>
+      switch (tangle(dp, denv, fp, fenv)) {
+      | None => false
+      | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc)
+      }
     | (FixF(dp, dc, None), _) =>
       let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv);
       matches_exp(~denv, dc, ~fenv, f);
@@ -213,33 +240,11 @@ let rec matches_exp =
     | (Fun(_), _) => false
 
     | (Let(dp, d1, d2), Let(fp, f1, f2)) =>
-      let dvars = DHPat.bound_vars(dp);
-      let fvars = DHPat.bound_vars(fp);
-      if (List.length(dvars) != List.length(fvars)) {
-        false;
-      } else {
-        let ids =
-          Array.init(List.length(dvars), _ => {
-            alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4))
-          });
-        let denv_subst: list((string, 'a)) =
-          List.mapi(
-            (i, binding) =>
-              (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
-            dvars,
-          );
-        let fenv_subst: list((string, 'a)) =
-          List.mapi(
-            (i, binding) =>
-              (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
-            fvars,
-          );
-        let denv =
-          evaluate_extend_env(Environment.of_list(denv_subst), denv);
-        let fenv =
-          evaluate_extend_env(Environment.of_list(fenv_subst), fenv);
-        matches_exp(d1, f1) && matches_exp(~denv, d2, ~fenv, f2);
-      };
+      switch (tangle(dp, denv, fp, fenv)) {
+      | None => false
+      | Some((denv, fenv)) =>
+        matches_exp(d1, f1) && matches_exp(~denv, d2, ~fenv, f2)
+      }
     | (Let(_), _) => false
 
     | (TypAp(d1, t1), TypAp(d2, t2)) =>
@@ -301,8 +306,12 @@ let rec matches_exp =
       && (
         switch (
           List.for_all2(
-            ((dk, dv), (fk, fv)) =>
-              matches_pat(dk, fk) && matches_exp(dv, fv),
+            ((dk, dv), (fk, fv)) => {
+              switch (tangle(dk, denv, fk, fenv)) {
+              | None => false
+              | Some((denv, fenv)) => matches_exp(~denv, dv, ~fenv, fv)
+              }
+            },
             drule,
             frule,
           )
@@ -362,58 +371,10 @@ and matches_fun =
   };
 }
 
-and matches_pat = (d: Pat.t, f: Pat.t): bool => {
-  switch (d |> DHPat.term_of, f |> DHPat.term_of) {
-  // Matt: I'm not sure what the exact semantics of matching should be here.
-  | (Parens(x), _) => matches_pat(x, f)
-  | (_, Parens(x)) => matches_pat(d, x)
-  | (Cast(x, _, _), _) => matches_pat(x, f)
-  | (_, Cast(x, _, _)) => matches_pat(d, x)
-  | (_, EmptyHole) => true
-  | (MultiHole(_), MultiHole(_)) => true
-  | (MultiHole(_), _) => false
-  | (Wild, Wild) => true
-  | (Wild, _) => false
-  | (Int(dv), Int(fv)) => dv == fv
-  | (Int(_), _) => false
-  | (Float(dv), Float(fv)) => dv == fv
-  | (Float(_), _) => false
-  | (Bool(dv), Bool(fv)) => dv == fv
-  | (Bool(_), _) => false
-  | (String(dv), String(fv)) => dv == fv
-  | (String(_), _) => false
-  | (ListLit(dl), ListLit(fl)) =>
-    switch (
-      List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl)
-    ) {
-    | exception (Invalid_argument(_)) => false
-    | res => res
-    }
-  | (ListLit(_), _) => false
-  | (Constructor(dt, _), Constructor(ft, _)) => dt == ft
-  | (Constructor(_), _) => false
-  | (Var(dx), Var(fx)) => String.equal(dx, fx)
-  | (Var(_), _) => false
-  | (Tuple(dl), Tuple(fl)) =>
-    switch (
-      List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl)
-    ) {
-    | exception (Invalid_argument(_)) => false
-    | res => res
-    }
-  | (Tuple(_), _) => false
-  | (Ap(d1, d2), Ap(f1, f2)) => matches_pat(d1, f1) && matches_pat(d2, f2)
-  | (Ap(_), _) => false
-  | (Cons(d1, d2), Cons(f1, f2)) =>
-    matches_pat(d1, f1) && matches_pat(d2, f2)
-  | (Cons(_), _) => false
-  | (EmptyHole, _) => false
-  | (Invalid(_), _) => false
-  };
-}
 and matches_typ = (d: Typ.t, f: Typ.t) => {
   Typ.eq(d, f);
 }
+
 and matches_utpat = (d: TPat.t, f: TPat.t): bool => {
   switch (d.term, f.term) {
   | (Invalid(_), _) => false