proposition: Lemma transportf_paths {X : UU} (P : X -> UU) {x1 x2 : X} {e1 e2 : x1 = x2} (e : e1 = e2) (p : P x1) : transportf P e1 p = transportf P e2 p.
proof: Proof. induction e. apply idpath. Defined.
imports: UniMath.Foundations.Preamble