proposition: Lemma xbindings_length m j acc : length (xbindings m j acc) = (cardinal m + length acc)%nat.
proof: Proof. revert j acc. induction m; simpl; trivial; intros. destruct o; simpl; rewrite IHm1; simpl; rewrite IHm2; now rewrite ?Nat.add_succ_r, Nat.add_assoc. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)