proposition: Lemma transport_idfun {X} (P:X->UU) {x y:X} (p:x = y) (u:P x) : transportf P p u = transportf (idfun UU) (maponpaths P p) u.
proof: Proof. intros. induction p. reflexivity. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics