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