Lemma weqoverdnicoprod_eq1' {n : nat} (P: ⟦S n⟧ → UU) jp : invmap (weqoverdnicoprod P) (ii1 jp) = (total2_base_map (dni lastelement) jp). Proof. intros. induction jp. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.