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