fact: Definition transport_pV {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P y) : p # p^ # z = z := (transport_pp P p^ p z)^ @ ap (fun r => transport P r z) (concat_Vp p).
imports: Basics.Overture Basics.Tactics