proposition: Lemma update_equiv : FEquiv t (t [a >- b ]).
proof: Proof. unfold FEquiv. intros x y. split; intro H. induction H. apply rzero. eauto. destruct (eq_num_dec i a). subst. assert (r=b). eapply repr_inj_right. eapply rsucc. apply H. auto. auto. subst. eapply rsucc. 2 : apply rzero. map_iff. tauto. eauto. eapply rsucc. 2 : apply IHrepr. map_iff. intuition. induction H. apply rzero. revert H. map_iff. intros. intro H'. apply H. auto. revert H. map_iff. intros [[H' H''] | H']. subst. assert (j = r). eapply repr_inj_idem; eauto. subst. eauto. destruct H'. eapply rsucc; eauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)