proposition: Lemma eq_bintreeP : Equality.axiom eq_bintree.
proof: Proof. move=> t1 t2; apply: (iffP idP) => [|<-]; last by elim: t1 => //= r -> l ->. elim: t1 t2 => [|l1 IHl r1 IHr]; first by case. by case=> //= l2 r2 /andP[Hr Hl]; rewrite (IHl _ Hr) (IHr _ Hl). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype