+Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+ forall v1 v2,
+ distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
+ mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) =
+ mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+ induction varstypes; intros.
+ destruct a; simpl; [ idtac | reflexivity ].
+ destruct p.
+ simpl.
+ simpl in H.
+ induction (leaves v1).
+ simpl; auto.
+ destruct (eqd_dec v v); auto.
+ assert False. apply n. auto. inversion H0.
+ simpl.
+ destruct a.
+ destruct (eqd_dec v0 v); subst; auto.
+ simpl in H.
+ rewrite map_app in H.
+ simpl in H.
+ rewrite nil_app in H.
+ apply distinct_swap in H.
+ rewrite app_ass in H.
+ apply distinct_app in H.
+ destruct H.
+ apply distinct_swap in H0.
+ simpl in H0.
+ inversion H0; subst.
+ assert False.
+ apply H3.
+ simpl; left; auto.
+ inversion H1.
+ apply IHl.
+ simpl in H.
+ inversion H; auto.
+ set (IHvarstypes1 v1 (varstypes2,,v2)) as i1.
+ set (IHvarstypes2 (v1,,varstypes1) v2) as i2.
+ simpl in *.
+ rewrite <- i1.
+ rewrite <- i2.
+ rewrite ass_app.
+ rewrite ass_app.
+ rewrite ass_app.
+ rewrite ass_app.
+ reflexivity.
+ clear i1 i2 IHvarstypes1 IHvarstypes2.
+ repeat rewrite ass_app in *; auto.
+ clear i1 i2 IHvarstypes1 IHvarstypes2.
+ repeat rewrite ass_app in *; auto.
+ Qed.