Definition helper_B {T} {Y} (f:T->Y) {y y':Y} (k:∏ t, y = f t) (e:y = y') t : transportf (λ y, y = f t) e (k t) = (transportf (λ y, ∏ t, y = f t) e k) t. Proof. intros. exact (helper_A _ k e t). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.