proposition: Lemma cp_pathscomp0 (A:Type) (B:A->Type) (a1 a2:A) (b1:B a1) (b2:B a2) (p q r:a1=a2) (α : p=q) (β : q=r) (s : PathOver p b1 b2) : cp (b1:=b1) (b2:=b2) (α @ β) s = cp β (cp α s).
proof: Proof. now induction α. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA