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