let h' := h.inv
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
⊢ Homotopy q p
V : Sort u_1
C : CombinatorialTwoComplex V
u v : V
p q r : Path u v
h : NullHomotopy (append p (inverse q))
h' : NullHomotopy (Loop.inv (append p (inverse q))) := NullHomotopy.inv h
⊢ Homotopy q p