Definition transportb2 {X} {Y:X->Type} (Z:∏ x, Y x->Type) {x x'} (p:x=x') (y':Y x') (z':Z x' y') : Z x (p#'y'). Proof. intros. induction p. exact z'. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.