diff --git a/lib/steel/pulse/Pulse.Typing.Metatheory.Base.fst b/lib/steel/pulse/Pulse.Typing.Metatheory.Base.fst
index 6383b548f..0286bf07f 100644
--- a/lib/steel/pulse/Pulse.Typing.Metatheory.Base.fst
+++ b/lib/steel/pulse/Pulse.Typing.Metatheory.Base.fst
@@ -266,7 +266,15 @@ let rec st_typing_weakening g g' t c d g1
 
     T_If _ b e1 e2 c uc hyp (magic ()) d_e1 d_e2 (magic ())
   
-  | T_Match _ sc_u sc_ty sc d_sc_ty d_sc c brs d_brs d_pats_complete -> magic ()
+  | T_Match _ sc_u sc_ty sc d_sc_ty d_sc c brs d_brs d_pats_complete ->
+    admit();
+    T_Match (push_env (push_env g g1) g')
+            sc_u sc_ty sc
+            (tot_typing_weakening g g' _ _ d_sc_ty g1)
+            (tot_typing_weakening g g' _ _ d_sc g1)
+            c brs
+            d_brs
+            d_pats_complete
 
   | T_Frame _ e c frame _ d_e ->
     T_Frame _ e c frame (magic ()) (st_typing_weakening g g' e c d_e g1)
diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml b/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml
index e831126f9..1f7c22734 100644
--- a/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml
+++ b/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml
@@ -381,7 +381,11 @@ let rec (st_typing_weakening :
               | Pulse_Typing.T_Match
                   (uu___, sc_u, sc_ty, sc, d_sc_ty, d_sc, c1, brs, d_brs,
                    d_pats_complete)
-                  -> Prims.magic ()
+                  ->
+                  Pulse_Typing.T_Match
+                    ((Pulse_Typing_Env.push_env
+                        (Pulse_Typing_Env.push_env g g1) g'), sc_u, sc_ty,
+                      sc, (), (), c1, brs, d_brs, d_pats_complete)
               | Pulse_Typing.T_Frame (uu___, e, c1, frame, uu___1, d_e) ->
                   Pulse_Typing.T_Frame
                     ((Pulse_Typing_Env.push_env