+Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+ not (In v (map (@fst _ _) varstypes)) ->
+ (update_ξ ξ lev varstypes) v = ξ v.
+ intros.
+ induction varstypes.
+ reflexivity.
+ simpl.
+ destruct a.
+ destruct (eqd_dec v0 v).
+ subst.
+ simpl in H.
+ assert False.
+ apply H.
+ auto.
+ inversion H0.
+ apply IHvarstypes.
+ unfold not; intros.
+ apply H.
+ simpl.
+ auto.
+ Defined.