Definition weqstnsum_invmap_step2 {n : nat} (f : ⟦S n⟧ -> nat) (k : ⟦f lastelement⟧) : weqstnsum_invmap f (weqfromcoprodofstn_map (stnsum (λ x, f (dni lastelement x))) (f lastelement) (ii2 k)) = (lastelement,,k). Proof. intros. unfold weqstnsum_invmap at 1. unfold nat_rect at 1. rewrite weqfromcoprodofstn_eq1. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.