proposition: Lemma xbindings_nil m p l : xbindings m p l = nil <-> is_empty m = true /\ l = nil.
proof: Proof. revert p l. induction m; simpl; intros; try easy. destruct o; now rewrite <- ?andb_lazy_alt, ?andb_true_iff, IHm1, ?IHm2. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)