proposition: 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 : pr1 bc1 = transportb _ ea (pr1 bc2)) (ec : pr2 bc1 = transportb C (total2_paths2_b ea eb) (pr2 bc2)) : bc1 = transportb BC ea bc2.
proof: Proof. destruct ea, bc1 as [b1 c1], bc2 as [b2 c2]. cbn in eb; destruct eb; cbn in ec; destruct ec. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics