proposition: Lemma transportb_fun' {X:UU} {P:X->UU} {Z:UU} {x x':X} (f:P x'->Z) (p:x=x') (y:P x) : f (transportf P p y) = transportb (λ x, P x->Z) p f y.
proof: Proof. intros. induction p. apply idpath. Defined.
imports: UniMath.Foundations.Preamble