Definition transportb_pair X (Y:X->Type) (Z:∏ x, Y x->Type) x x' (p:x = x') (y':Y x') (z':Z x' y') (z'' : (Z x' y')) : transportb (λ x, total2 (Z x)) p (tpair (Z x') y' z') = tpair (Z x) (transportb Y p y') (transportb2 _ p y' z'). Proof. intros. induction p. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.