rw [Path.append_assoc p _ _, ← Path.append_assoc _ q _] at H
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append (append p (inverse q)) (append q (inverse r))) := NullHomotopy.concat h h'
⊢ Homotopy p r
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (append q (inverse r))
H : NullHomotopy (append p (append (append (inverse q) q) (inverse r)))
⊢ Homotopy p r