{A} {P : A -> Type} {a0 a1} {p : a0 = a1} {b0 : P a0} {b1 b2 : P a1} : DPath P p b0 b1 -> (b1 = b2) -> DPath P p b0 b2. Proof. destruct p; exact concat. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.