Lemma total2_reassoc_paths {A} {B : A → UU} {C : (∑ a, B a) -> UU} (BC : A -> UU := λ a, ∑ b, C (a,,b)) {a1 a2 : A} (bc1 : BC a1) (bc2 : BC a2) (ea : a1 = a2) (eb : transportf _ ea (pr1 bc1) = pr1 bc2) (ec : transportf C (two_arg_paths_f ea eb) (pr2 bc1) = pr2 bc2) : transportf _ ea bc1 = bc2. Proof. destruct bc1 as [b1 c1], bc2 as [b2 c2]; simpl in *. destruct ea. destruct eb. simpl in *. destruct ec. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.