exact NullHomotopy.splice b a
V : Sort u_1
C : CombinatorialTwoComplex V
u✝ v✝ : V
p✝ q✝ r✝ : Path u✝ v✝
u v w : V
p q : Path u v
r s : Path v w
a : NullHomotopy (append p (inverse q))
b : NullHomotopy (append r (inverse s))
⊢ NullHomotopy (append p (append (append r (inverse s)) (inverse q)))
no goals