Definition helper_D m n : isweq (helper_B m n). Proof. intros. simple refine (isweq_iso _ (helper_C _ _) _ _). { intro e. assert(p := ! helper_B _ _ e). destruct p. apply proofirrelevancecontr. apply nat_discern_iscontr. } { intro e. destruct e. induction m as [|m IHm]. { reflexivity. } { exact ( maponpaths (helper_B (S m) (S m)) (! apSC _ _ (idpath m)) @ maponpaths (maponpaths S) IHm). } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.