diff --git a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda
index 1214b95c1..f1f349326 100644
--- a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda
+++ b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda
@@ -230,7 +230,6 @@ Bool⋀→ {A = A} (push (inr x) i) = pt A
 Bool⋀→ {A = A} (push (push a i₁) i) = pt A
 
 ⋀lIdIso : Iso (Bool*∙ {ℓ} ⋀ A) (typ A)
-Iso.fun (⋀lIdIso {A = A}) (inl x) = pt A
 Iso.fun ⋀lIdIso = Bool⋀→
 Iso.inv ⋀lIdIso a = inr (false* , a)
 Iso.rightInv ⋀lIdIso a = refl