+Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
+ intros.
+ induction b.
+ rewrite <- app_nil_end in H; auto.
+ rewrite <- app_comm_cons.
+ set (distinct_lemma _ _ _ H) as H'.
+ set (IHb H') as H''.
+ apply distinct_cons; [ idtac | apply H'' ].
+ intros.
+ apply in_both in H0.
+ clear H'' H'.
+ destruct H0.
+ apply distinct_app in H.
+ destruct H.
+ inversion H1; auto.
+ clear IHb.
+ rewrite nil_app in H.
+ rewrite ass_app in H.
+ apply distinct_app in H.
+ destruct H; auto.
+ apply distinct_swap' in H.
+ inversion H; auto.
+ Qed.
+
+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.
+
+Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+ distinct (map (@fst _ _) (leaves varstypes)) ->
+ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
+ mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+ set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q.
+ simpl in q.
+ rewrite <- app_nil_end in q.
+ apply q.
+ Qed.