fact: Definition inverse_cp_p (A:Type) (B:A->Type) (a1 a2:A) (b1:B a1) (b2:B a2) (p q:a1=a2) (α : p=q) (t : PathOver p b1 b2) : cp (! α) (cp α t) = t.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA