diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 73d58e3a7d..dcbe6db9b4 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -44,6 +44,7 @@ import qualified Cryptol.Eval.Value as V
 import qualified Cryptol.Eval.Concrete as V
 import Cryptol.Eval.Type (evalValType)
 import qualified Cryptol.TypeCheck.AST as C
+import qualified Cryptol.TypeCheck.SimpType as ST
 import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, singleTParamSubst)
 import qualified Cryptol.ModuleSystem.Name as C
   (asPrim, asParamName, nameUnique, nameIdent, nameInfo, NameInfo(..))
@@ -230,10 +231,11 @@ importPC sc pc =
     C.PFLiteral        -> panic "importPC PFLiteral" []
     C.PValidFloat      -> panic "importPC PValidFloat" []
 
--- | Translate size types to SAW values of type Num, value types to SAW types of sort 0.
+-- | Normalize according to Cryptol's rules, then translate size types to SAW
+-- values of type Num and value types to SAW types of sort 0.
 importType :: SharedContext -> Env -> C.Type -> IO Term
 importType sc env ty =
-  case ty of
+  case ST.tRebuild ty of
     C.TVar tvar ->
       case tvar of
         C.TVFree{} {- Int Kind (Set TVar) Doc -} -> unimplemented "TVFree"
diff --git a/intTests/test_join_split/README.md b/intTests/test_join_split/README.md
new file mode 100644
index 0000000000..03180efab4
--- /dev/null
+++ b/intTests/test_join_split/README.md
@@ -0,0 +1,7 @@
+This test addresses the issue resolved in [#1790](https://github.com/GaloisInc/saw-script/pull/1790). 
+
+In this script, we prove the same theorem - that ```join`{each=32, parts=4, a=Bool} (split x) == x``` - twice; once purely via `z3`, and once via manual rewriting, trying to use the former to prove the latter. 
+
+Lack of type normalization introduces reflexive type coercions in the SAWCore representation of the expression under proof. The manual proof proceeds by eliminating any extant reflexive coercions, then attempting to use the `z3`-proven theorem as a simplification. When no coercions existed in the first place, the simplification applies cleanly. When coercions existed, the simplification does not apply cleanly, since we eliminated them from the goal, but not from the simplification.
+
+Since this proof is possible to resolve in its entirety via evaluation/appeal to `z3`, we need to maintain the core `join` and `split` functions uninterpreted when manually massaging (via `goal_normalize` and `goal_eval_unint`) the goal into a `trivial`ly resolvable form.
\ No newline at end of file
diff --git a/intTests/test_join_split/join_split.saw b/intTests/test_join_split/join_split.saw
new file mode 100644
index 0000000000..455b68aafa
--- /dev/null
+++ b/intTests/test_join_split/join_split.saw
@@ -0,0 +1,10 @@
+enable_experimental; // for `goal_normalize`
+
+join_split_thm_z3 <- prove_print z3 {{ \x -> join`{each=32, parts=4, a=Bool} (split x) == x }};
+
+join_split_thm_manual <- prove_print (do {
+    goal_normalize ["ecJoin", "ecSplit"];
+    simplify (addsimp join_split_thm_z3 empty_ss);
+    goal_eval_unint ["ecJoin", "ecSplit"];
+    trivial;
+}) {{ \x -> join`{each=32, parts=4, a=Bool} (split x) == x }};
diff --git a/intTests/test_join_split/test.sh b/intTests/test_join_split/test.sh
new file mode 100644
index 0000000000..deed8e9fc4
--- /dev/null
+++ b/intTests/test_join_split/test.sh
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+$SAW join_split.saw
\ No newline at end of file