Lemma apSC m n (e:m=n) : helper_C m n e = helper_C (S m) (S n) (maponpaths S e). Proof. intros. apply proofirrelevance. apply nat_discern_isaprop. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.