proposition: Lemma bintree_of_Dyck_spec D : { t : bintree | Dyck_of_bintree t = D /\ forall t', Dyck_of_bintree t' = D -> t = t' }.
proof: Proof. elim/Dyck_ind: D => [|D1 D2 [t1 [PF1 Uniq1]] [t2 [PF2 Uniq2]]]. by exists BinLeaf; split; last by case. exists (BinNode t1 t2); split => /=; first by rewrite PF1 PF2. by case => //= t'1 t'2 /join_Dyck_inj => [[/Uniq1 -> /Uniq2 ->]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree