proposition: Lemma cons_TamariP v : v \is a TamariVector -> size v :: v \is a TamariVector.
proof: Proof. move=> H; apply/Tamari_consP; split => // i Hi. by move: H => /TamariP[H _]; apply H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype