proposition: Lemma D_update : forall x y t, x <> y -> D t y 0 -> D (t [x>- y]) y 0.
proof: Proof. intros x y t' Hxy H. rewrite D_repr. apply rzero. map_iff. intros [H' | H']; [ subst; tauto_false | inversion H ; eauto ]. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)