proposition: Lemma treeify_mapsto x v l : (treeify l)@x ↦ v <-> InA O.eqke (x,v) l.
proof: Proof. intros. now rewrite <- bindings_spec1, treeify_bindings. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)