diff --git a/.github/workflows/build_2021-1.yml b/.github/workflows/build_2021-1.yml
deleted file mode 100644
index e6b24f0..0000000
--- a/.github/workflows/build_2021-1.yml
+++ /dev/null
@@ -1,15 +0,0 @@
-on: [push]
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    name: Build Theory
-    steps:
-      - uses: actions/checkout@v3
-      - uses: lexbailey/isabelle-theory-build-github-action@v7
-        with:
-          isabelle-version: '2021-1'
-          custom-isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/tags/itrees_utp_2021-1.zip'
-          depends: 'https://github.com/isabelle-utp/Shallow-Expressions.git@main https://github.com/isabelle-utp/explore-subgoal.git@main'
-          session-name: 'Interaction_Trees ITree_Simulation ITree_UTP ITree_VCG ITree_RoboChart'
-          report_url: 'https://isabelle-utp-ci-dashboard.link/submit_job_log'
-          report_secret: ${{ secrets.DashboardReportKey }}
diff --git a/.github/workflows/build_2022.yml b/.github/workflows/build_2023.yml
similarity index 65%
rename from .github/workflows/build_2022.yml
rename to .github/workflows/build_2023.yml
index 26955a7..e0f2184 100644
--- a/.github/workflows/build_2022.yml
+++ b/.github/workflows/build_2023.yml
@@ -5,12 +5,12 @@ jobs:
     name: Build Theory
     steps:
       - uses: actions/checkout@v3
-      - uses: lexbailey/isabelle-theory-build-github-action@v7
+      - uses: lexbailey/isabelle-theory-build-github-action@v9
         with:
-          isabelle-version: '2022'
-          custom-isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/heads/itrees_utp_2022.zip'
-          depends: 'https://github.com/isabelle-utp/Shallow-Expressions.git@main https://github.com/isabelle-utp/explore-subgoal.git@main'
+          isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/tags/CyPhyAssure2023.tar.gz'
+          depends: 'https://github.com/isabelle-utp/Shallow-Expressions.git@main https://github.com/isabelle-utp/explore-subgoal.git@main https://github.com/isabelle-utp/Abstract_Prog_Syntax.git@main'
           session-name: 'Interaction_Trees ITree_Simulation ITree_UTP ITree_VCG ITree_RoboChart'
           report_url: 'https://isabelle-utp-ci-dashboard.link/submit_job_log'
           report_secret: ${{ secrets.DashboardReportKey }}
+     
 
diff --git a/UTP/ITree_Relation.thy b/UTP/ITree_Relation.thy
index 85d10ca..51c4201 100644
--- a/UTP/ITree_Relation.thy
+++ b/UTP/ITree_Relation.thy
@@ -101,6 +101,13 @@ lemma promote_rel [itree_pred]:
   by (auto elim!: trace_to_bindE bind_RetE' simp add: itree_pred_def retvals_def promote_itree_def lens_override_def)
      (metis bind_Ret trace_to_bind_left)
 
+lemma itree_pred_match [simp]: 
+  "match_itree (e)\<^sub>e (case_option P Q) = (if e = None then P else (let v \<leftarrow> the e in Q v) fi)" 
+  by (simp add: match_itree_def let_itree_def cond_itree_def option.case_eq_if fun_eq_iff)
+
+lemma let_itree_pred [itree_pred]: "\<lbrakk>let_itree e P\<rbrakk>\<^sub>p = (\<lambda> (s, s'). let v = e s in \<lbrakk>P v\<rbrakk>\<^sub>p (s, s'))"
+  by (simp add: let_itree_def itree_pred_def)
+
 ML_file \<open>Lens_Rel_Utils.ML\<close>
 
 method rename_rel_alpha_vars = tactic \<open> Lens_Rel_Utils.rename_rel_alpha_vars \<close>