proposition: Lemma treeify_bindings l : bindings (@treeify elt l) = l.
proof: Proof. assert (H := @treeify_aux_spec (plength l) true l). unfold treeify. destruct treeify_aux as (t,acc); simpl in *. destruct H as (H,H'). { now rewrite plength_spec. } subst l. rewrite plength_spec, app_length, <- cardinal_spec in *. destruct acc. * now rewrite app_nil_r. * exfalso. revert H. simpl. rewrite Nat.add_succ_r, Nat.add_comm. apply Nat.succ_add_discr. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)