diff --git a/formalizations/guarded-cubical/Syntax/Normalization.agda b/formalizations/guarded-cubical/Syntax/Normalization.agda
index 0dce3e0d041600b787de68e4704e90c379480fac..46225c9330849d0de53fce1ebadb07ebe946baf2 100644
--- a/formalizations/guarded-cubical/Syntax/Normalization.agda
+++ b/formalizations/guarded-cubical/Syntax/Normalization.agda
@@ -218,7 +218,7 @@ unVNfm-subst {Γ = Γ} (lda {S = S}{R = R} M) γ =
   cong Syntax.IntensionalTerms.lda ((unCNfm-subst M (↑snf γ)) ∙ cong (unCNfm M [_]c) (cong (_,s var) (unSNfm-wk γ)))
   -- Unfortunately the solver can't prove this as written because it wants to pattern match on M
   -- We would need to add some support for uninterpreted function symbols in the solver to get this.
-  ∙ {!!}
+  ∙ sym (lda-nat _ _)
 unVNfm-subst zro γ = Nbe.by-vsimpl refl
 unVNfm-subst (suc V) γ = cong (suc [_]v) (cong (!s ,s_) (unVNfm-subst V γ))
   ∙ Nbe.by-vsimpl refl