proposition: Lemma append_mapsto l r y v : (append l r)@y ↦ v <-> l@y ↦ v \/ r@y ↦ v.
proof: Proof. revert r. append_tac l r; try (intuition_m; fail). - simpl. destmatch. + intuition_m. + rewrite mapsto_2levels. factornode m. rewrite !node_mapsto, !leaf_mapsto. rtauto. + factornode m. rewrite !node_mapsto. rtauto. - simpl. destmatch; rewrite ?lbalS_mapsto. + intuition_m. + rewrite mapsto_2levels. factornode m. rewrite !node_mapsto, !leaf_mapsto. rtauto. + factornode m. rewrite !node_mapsto. rtauto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)