diff --git a/formalizations/guarded-cubical/Syntax/Normalization.agda b/formalizations/guarded-cubical/Syntax/Normalization.agda
index 57297c32d18b68d8493fe1250f1a444bf497b4d1..df2c00a02d796aa9105a6d2a98c0356490831db9 100644
--- a/formalizations/guarded-cubical/Syntax/Normalization.agda
+++ b/formalizations/guarded-cubical/Syntax/Normalization.agda
@@ -239,3 +239,10 @@ cases .indbind {M = M} = rec (isPropΠ λ _ → squash₁) λ ihN[x] ihM →
 
 readOut : ∥ fiber unCNfm M ∥₁ → singl M
 readOut = rec isPropSingl (λ x → (unCNfm (x .fst)) , (sym (x .snd)))
+
+csimpl : Comp Γ R → Comp Γ R
+csimpl M = fst (readOut (Sem.indPc cases M))
+
+csimpl-eq : (M : Comp Γ R) → M ≡ csimpl M
+csimpl-eq M = snd (readOut (Sem.indPc cases M))
+