fact: Definition dp_const_pp {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).
imports: Basics Types.Paths Types.Sigma Types.Forall