Definition weqoverdnicoprod {n : nat} (P: ⟦S n⟧ → UU) : (∑ i, P i) ≃ (∑ j, P(dni lastelement j)) ⨿ P lastelement. Proof. intros. use (weqcomp (weqtotal2overcoprod' P (weqdnicoprod n lastelement))). apply weqcoprodf. - apply idweq. - apply weqtotal2overunit. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.