{A B : Type} {a0 a1 a2 : A} {p : a0 = a1} {q : a1 = a2} {x y z : B} (r : x = y) (s : y = z) : dp_const (p:=p @ q) (r @ s) = (dp_const (p:=p) r) @Dp (dp_const (p:=q) s). Proof. by destruct p,q. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.