let H' := NullHomotopy.contract (.swap $ .trivial _) 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 p (append (append (inverse q) q) (inverse r)))
⊢ 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)))
H' : NullHomotopy (append p (inverse r)) := NullHomotopy.contract (NullHomotopy.swap (NullHomotopy.trivial q)) H
⊢ Homotopy p r