dp_apD_const' {A B : Type} {f : A -> B} {a0 a1 : A} {p : a0 = a1} : dp_const^-1 (apD f p) = ap f p. Proof. apply moveR_equiv_V. apply dp_apD_const. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.