DPath (fun t : a0 = a3 => DPath P t b0 b3) (concat_p_pp p q r) (dp @Dp (dq @Dp dr)) ((dp @Dp dq) @Dp dr). Proof. destruct p, q, r. apply concat_p_pp. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.