proposition: Lemma DP_FT_DH1_unique d1 d2: all DP_FT_DH1 d1 -> all DP_FT_DH1 d2 -> flatten d1 = flatten d2 -> d1 = d2.
proof: Proof. move => pa pb; apply:DP_FT_DH1aux_unique; rewrite /DP_resizeb_condition. + by move: pa;case: d1 => // b l /=; move/andP => [-> ->]. + by move: pb;case: d2 => // b l /=; move/andP => [-> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)