title: Cube with different combinations of refl in cubical agda
body: <p>I am working on the following lemma but the proof is starting to grow longer, and longer.</p>
  
  <pre><code>assoc-lUnit-rUnit-refl-lemma : ∀ {ℓ} → {A : Type ℓ} → {x : A}
             → (assoc refl refl refl) 
                ≡ 
               sym (lUnit (refl {x = x} ∙ refl)) ∙ (rUnit (refl ∙ refl))
  </code></pre>
  
  <p>It refers to definitions in the cubical library in file <a href="https://github.com/agda/cubical/blob/265294a703b821fea92a8cab1589030963dff4e7/Cubical/Foundations/GroupoidLaws.agda" rel="nofollow noreferrer">GrupoidLaws.agda</a></p>
  
  <p>I do not necessarily expect whole proof here, just some advice. 
  Should I expect this proof to be straightforward thanks to refl everywhere?
  Or do I have to basically follow back all definitions inside lUnit, rUnit, and assoc,
  because refl does not force any computation?</p>