proposition: Lemma find_equiv : forall n s t x y t' px, find_aux n x t = (y,t') -> D t x px -> px < n -> bounded t s -> ( D t' y O /\ (x = y \/ NumMap.MapsTo x y t') /\ FEquiv t t' /\ bounded t' s ).
proof: Proof. induction n; intros s t0 x y t' px Hxt Hx Hpx Hwf. lia_false. simpl in Hxt. find_analyse. case_eq (find_aux n x0 t0). intros p' t'' H'. rewrite H' in *. injection Hxt. intros. subst. clear Hxt. destruct (D_succ _ _ _ _ H Hx). subst . destruct (IHn s _ _ _ _ _ H' H0) as [Hy [[Hxy | Hxy] [Heq Hwf']] ] . lia. auto. subst. assert (x <> y). eapply D_inv_n. 2:eauto. rewrite FEquiv_D; eauto. assert (repr t'' x y). rewrite <- Heq. eapply rsucc; eauto. rewrite <- D_repr. rewrite FEquiv_D; eauto. split; simpl. apply D_update; auto. split. right; map_iff; auto. split. rewrite Heq; apply update_equiv; auto. apply boundage; auto. assert (x <> y). eapply (D_inv_n t0); eauto. rewrite FEquiv_D; eauto. assert (repr t'' x y). rewrite <- Heq. eapply rsucc; eauto. rewrite Heq. eapply rsucc; eauto. rewrite <- D_repr. auto. split; simpl. eapply D_update; eauto. split. right; map_iff; auto. split. rewrite Heq; apply update_equiv; auto. apply boundage; auto. dependent destruction Hxt. intuition. rewrite D_repr. eapply rzero. eauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)