proposition: Lemma from_vct_cat u v t : u \is a TamariVector -> from_vct_acc t (u ++ v) = from_vct_acc (from_vct_acc t u) v.
proof: Proof. rewrite /from_vct => /from_vctK <-. rewrite -(left_branchK (from_vct u)). elim/last_ind: (left_branch _) t => [| br bn IHbr] //= t. rewrite right_sizes_from_left rev_rcons /= -right_sizes_from_left. rewrite !from_vct_accE -catA. rewrite !take_size_cat ?size_right_sizes //. by rewrite !drop_size_cat ?size_right_sizes //. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype