(A : Type) (P : A -> Type) (f : forall a, P a) {a0 a1 : A} (p : a0 = a1) : apD f p^ = (apD f p)^D. Proof. by destruct p. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.