{A B : Type} {a0 a1 : A} {p : a0 = a1} {x y : B} (r : x = y) : dp_const r^ = (dp_const (p:=p) r)^D. Proof. by destruct p. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.