Lemma weqstnsum1_step {n : nat} (f : ⟦S n⟧ -> nat) : ( weqstnsum1_prelim f = weqfromcoprodofstn (stnsum (funcomp (dni lastelement) f)) (f lastelement) ∘ (weqcoprodf1 (weqstnsum1_prelim (λ i, f (dni lastelement i))) ∘ weqoverdnicoprod (λ i, ⟦ f i ⟧))) % weq. Proof. intros. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.