{A} {P : A -> Type} {a0 a1 a2} {p : a0 = a1} {q : a1 = a2} {b0 : P a0} {b1 : P a1} {b2 : P a2} {r r' : DPath P p b0 b1} {s s' : DPath P q b1 b2} (h : r = r') (k : s = s') : r @Dp s = r' @Dp s'. Proof. by destruct h, k. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.