Definition from_total2 {X} {P:X->Type} {Y} : (∏ x, P x->Y) -> total2 P -> Y. Proof. intros f [x p]. exact (f x p). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.