diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index dbe0724dc..cfed932e0 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -552,6 +552,7 @@ namespace eq
 
   definition square_fill_r : Σ (p : a₂₀ = a₂₂) , square p₁₀ p₁₂ p₀₁ p :=
   by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩
+  variables {p₁₀ p₁₂ p₀₁ p₂₁}
 
   /- Squares having an 'ap' term on one face -/
   --TODO find better names