Cube with different combinations of refl in cubical agda

Question

I am working on the following lemma but the proof is starting to grow longer, and longer.

assoc-lUnit-rUnit-refl-lemma : ∀ {ℓ} → {A : Type ℓ} → {x : A}
           → (assoc refl refl refl) 
              ≡ 
             sym (lUnit (refl {x = x} ∙ refl)) ∙ (rUnit (refl ∙ refl))

It refers to definitions in the cubical library in file GrupoidLaws.agda

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?