+ Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) l1 l2 q,
+ update_ξ ξ (app l1 l2) q = update_ξ (update_ξ ξ l2) l1 q.
+ intros.
+ induction l1.
+ reflexivity.
+ simpl.
+ destruct a; simpl.
+ rewrite IHl1.
+ reflexivity.
+ Qed.
+
+ Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
+ intros.
+ induction t.
+ destruct a; auto.
+ simpl; rewrite H; auto.
+ simpl; rewrite IHt1; rewrite IHt2; auto.
+ Qed.
+
+ Lemma quark {T} (l1:list T) l2 vf :
+ (In vf (app l1 l2)) <->
+ (In vf l1) \/ (In vf l2).
+ induction l1.
+ simpl; auto.
+ split; intro.
+ right; auto.
+ inversion H.
+ inversion H0.
+ auto.
+ split.
+
+ destruct IHl1.
+ simpl in *.
+ intro.
+ destruct H1.
+ left; left; auto.
+ set (H H1) as q.
+ destruct q.
+ left; right; auto.
+ right; auto.
+ simpl.
+
+ destruct IHl1.
+ simpl in *.
+ intro.
+ destruct H1.
+ destruct H1.
+ left; auto.
+ right; apply H0; auto.
+ right; apply H0; auto.
+ Qed.
+
+ Lemma splitter {T} (l1:list T) l2 vf :
+ (In vf (app l1 l2) → False)
+ -> (In vf l1 → False) /\ (In vf l2 → False).
+ intros.
+ split; intros; apply H; rewrite quark.
+ auto.
+ auto.
+ Qed.
+
+ Lemma helper
+ : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
+ (In vf (leaves tl) -> False) ->
+ mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
+ mapOptionTree ξ tl.
+ intros.
+ induction tl;
+ try destruct a;
+ simpl in *.
+ set (eqd_dec vf t) as x in *.
+ destruct x.
+ subst.
+ assert False.
+ apply H.
+ left; auto.
+ inversion H0.
+ auto.
+ auto.
+ apply splitter in H.
+ destruct H.
+ rewrite (IHtl1 H).
+ rewrite (IHtl2 H0).
+ reflexivity.
+ Qed.
+
+ Lemma fresh_lemma' Γ
+ : forall types vars Σ ξ, Σ = mapOptionTree ξ vars ->
+ FreshM { varstypes : _
+ | mapOptionTree (update_ξ(Γ:=Γ) ξ (leaves varstypes)) vars = Σ
+ /\ mapOptionTree (update_ξ ξ (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = types }.
+ induction types.
+ intros; destruct a.
+ refine (bind vf = fresh (leaves vars) ; return _).
+ apply FreshMon.
+ destruct vf as [ vf vf_pf ].
+ exists [(vf,l)].
+ split; auto.
+ simpl.
+ set (helper VV _ vars vf ξ l vf_pf) as q.
+ rewrite q.
+ symmetry; auto.
+ simpl.
+ destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
+ refine (return _).
+ exists []; auto.
+ intros vars Σ ξ pf; refine (bind x2 = IHtypes2 vars Σ ξ pf; _).
+ apply FreshMon.
+ destruct x2 as [vt2 [pf21 pf22]].
+ refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,types2) (update_ξ ξ (leaves vt2)) _; return _).
+ apply FreshMon.
+ simpl.
+ rewrite pf21.
+ rewrite pf22.
+ reflexivity.
+ clear IHtypes1 IHtypes2.
+ destruct x1 as [vt1 [pf11 pf12]].
+ exists (vt1,,vt2); split; auto.
+
+ set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q.
+ set (mapOptionTree_extensional _ _ q) as q'.
+ rewrite q'.
+ clear q' q.
+ inversion pf11.
+ reflexivity.
+
+ simpl.
+ set (update_branches Γ ξ (leaves vt1) (leaves vt2)) as q.
+ set (mapOptionTree_extensional _ _ q) as q'.
+ rewrite q'.
+ rewrite q'.
+ clear q' q.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose in *.
+ rewrite pf12.
+ inversion pf11.
+ rewrite <- mapOptionTree_compose.
+ reflexivity.
+ Defined.