Definition flattenStep' {X n} (m : stn (S n) → nat) (x : ∏ i : stn (S n), stn (m i) → X) (m' := m ∘ dni lastelement) (x' := x ∘ dni lastelement) : flatten' x = concatenate' (flatten' x') (x lastelement). Proof. intros. apply funextfun; intro i. unfold flatten'. unfold funcomp. rewrite 2 weqstnsum1_eq'. unfold StandardFiniteSets.weqstnsum_invmap at 1. unfold concatenate'. unfold nat_rect, coprod_rect, funcomp. change (weqfromcoprodofstn_invmap (stnsum (λ r : stn n, m (dni lastelement r)))) with (weqfromcoprodofstn_invmap (stnsum m')) at 1 2. induction (weqfromcoprodofstn_invmap (stnsum m')) as [B|C]. - reflexivity. - now induction C. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.