proposition: Lemma DP_FT_DH1aux_unique d1 d2: DP_resizeb_condition d1 -> DP_resizeb_condition d2 -> flatten d1 = flatten d2 -> d1 = d2.
proof: Proof. pose q x := (~~ nilp x && Dyck_NH1 x). have Ht a b u v: q a -> (prependFT b) ++ u = a ++ v -> false. move => /andP[sa sb] sc. suff sd: (starts_withFT a) by move:(DP_NH1_prop3 sd); rewrite sb. move: sa sb sc; case:a => // [] [] // [] // [] //. have W x (l: seq bool) n : x = take n l -> 2 <= size x -> take 2 x = take 2 l. move => ->; case:l=>// a; case; [by case:n | move => b l]; case:n=> [|n] //. by case:n=> //n; rewrite /=!take0. have He a b l1 (x:= take (size b - size a) (flatten l1)) : size a < size b -> Dyck_path a -> Dyck_path b -> all DP_FT_DH1 l1 -> b = a ++ x -> starts_withFT x. move => ha hb hc hd gf. rewrite starts_withFT_alt; rewrite gf in hc. have sx: 2 <= size x. move: ha; rewrite gf size_cat; move: (Dyck_sub_path hb hc). case x; [by rewrite addn0 ltnn | move => a1 [ | //]]; by case:a1. rewrite (W _ (flatten l1) (size b - size a) (erefl x) sx). move: hd sx; rewrite /x. clear. case: l1 => // aa ll /= /andP[/andP [he _] _]. by rewrite starts_withFT_prop in he; rewrite /= (eqP he) 2!cat_cons //= take0. rewrite /DP_resizeb_condition; case: d1;case: d2 => //. by case => //l; rewrite /DP_ph1_aux2 /= andbF. by case => // l; rewrite /DP_ph1_aux2 /= andbF. move => a l1 b l2 /=. suff aux: forall d1 d2, all DP_FT_DH1 d1 -> all DP_FT_DH1 d2 -> flatten d1 = flatten d2 -> d1 = d2. have sx x:(DP_FT_DH1 x || DP_ph1_aux2 x) = DP_FT_DH1 x || (q x). rewrite /DP_ph1_aux2 /q. by case xv: (x == DyckFT) => //; rewrite (eqP xv). rewrite sx sx. move => /andP [ha hb] /andP[hc hd]; case/orP:hb; case/orP:hd => hb hd. + by move => w; apply: aux => //=; [ rewrite ha hd | rewrite hb hc]. + move/andP:hd =>[]; rewrite starts_withFT_prop => /eqP -> _ sc. by move:(Ht a (drop 2 b)(flatten l2) (flatten l1) hb sc). + move/andP:hb =>[]; rewrite starts_withFT_prop => /eqP -> _ /esym sc. by move:(Ht b (drop 2 a)(flatten l1) (flatten l2) hd sc). + move => eq1. suff eab: a = b. by move: eq1; rewrite eab => /eqseq_cat1 hab; rewrite (aux _ _ ha hc hab). wlog lsab: a b l1 l2 ha hc hb hd eq1/ size a <= size b. move => hh; case /orP:(leq_total (size a) (size b)) => xx. by apply: (hh _ _ _ _ ha hc hb hd eq1 xx). symmetry; apply:(hh _ _ _ _ hc ha hd hb (esym eq1) xx). move: (f_equal (take (size b)) eq1); rewrite take_size_cat //. rewrite take_cat ltnNge lsab /=. move: lsab;rewrite leq_eqVlt => /orP; case => lsab. by rewrite (eqP lsab) subnn take0 cats0. set x := take (size b - size a) (flatten l1) => xp. have dpa: Dyck_path a by move/andP:hb => [_ /andP[]]. move/andP:hd => [_ ww]; move/andP:(ww) => [dpb _]. move: (He a b l1 lsab dpa dpb hc xp) => sftx. by move:(DP_NH1_prop4 dpa sftx); rewrite - xp ww. clear a b l1 l2. move => d1 d2. move En: (size d1 + size d2) => n. have: size d1 <= n by rewrite -En ; apply leq_addr. have: size d2 <= n by rewrite -En ; apply leq_addl. have T a l: all DP_FT_DH1 (a :: l) -> ~~ nilp (flatten (a :: l)). by move=> /= /andP[/andP[]]; case:a => //. elim: n d1 d2 {En}. by move => d1 d2; rewrite !leqn0 => /nilP -> /nilP. move => n Hr; case. by case => // a l _ _ _;move/T => sa sb; move: sa; rewrite - sb. move => a d1; case; first by move => _ _ /T sa _ sb ; move: sa; rewrite sb. move => b d2 /=;rewrite 2!ltnS; wlog:a d1 b d2 /size a <= size b. move => hh; case /orP:(leq_total (size a) (size b)); first by apply: hh. by move => sa sb sc ha hb /esym hc; symmetry; apply:hh. move => lsab sd2n sd1n /andP[ph1 ph2] /andP[ph3 ph4] sv {T}. suff eab: a = b. move /eqP: sv; rewrite eab eqseq_cat // eqxx /= => /eqP ha. by rewrite (Hr _ _ sd2n sd1n ph2 ph4 ha). move: (f_equal (take (size b)) (esym sv)); rewrite take_size_cat //. rewrite take_cat ltnNge lsab /=. move: lsab;rewrite leq_eqVlt => /orP; case => lsab. by rewrite (eqP lsab) subnn take0 cats0. move: ph1 ph3 lsab; rewrite /DP_FT_DH1 !starts_withFT_prop. move => /andP [/eqP {2 3 4} -> /andP [dpa pa]]. move=> /andP[/eqP {2 3 4} -> ww]; move/andP:(ww)=>[dpb pb]. rewrite /= 2!ltnS => lsab; case => xp. have sftx:= (He _ _ d1 lsab dpa dpb ph2 xp). by move:(DP_NH1_prop4 dpa sftx); rewrite - xp ww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)