+Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t.
+ induction x; simpl.
+ apply strip_nil_lemma.
+ rewrite strip_lemma.
+ rewrite IHx.
+ clear IHx.
+ rewrite <- strip_lemma.
+ reflexivity.
+ Qed.
+
+Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
+ intros.
+ induction y.
+ destruct a0; try reflexivity.
+ simpl in *.
+ unfold stripOutVars.
+ simpl.
+ destruct (eqd_dec v a).
+ subst.
+ assert False.
+ apply H.
+ left; auto.
+ inversion H0.
+ auto.
+ rewrite <- IHy1 at 2.
+ rewrite <- IHy2 at 2.
+ reflexivity.
+ unfold not; intro.
+ apply H.
+ eapply In_both' in H0.
+ apply H0.
+ unfold not; intro.
+ apply H.
+ eapply In_both in H0.
+ apply H0.
+ Qed.
+
+Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
+ intros.
+ induction x.
+ reflexivity.
+ simpl.
+ destruct (eqd_dec v a).
+ subst.
+ assert False. apply H.
+ simpl; auto.
+ inversion H0.
+ apply IHx.
+ unfold not.
+ intro.
+ apply H.
+ simpl; auto.
+ Qed.
+
+Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
+ induction a; intros.
+ simpl.
+ simpl in H.
+ apply In_both'.
+ auto.
+ rewrite <- ass_app.
+ rewrite <- app_comm_cons.
+ simpl.
+ rewrite ass_app.
+ rewrite <- app_comm_cons in H.
+ inversion H.
+ left; auto.
+ right.
+ apply IHa.
+ apply H0.
+ Qed.
+
+Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
+ induction a; intros.
+ simpl in *.
+ apply distinct_app in H; auto.
+ destruct H; auto.
+ rewrite <- app_comm_cons.
+ apply distinct_cons.
+ rewrite <- ass_app in H.
+ rewrite <- app_comm_cons in H.
+ inversion H.
+ subst.
+ intro q.
+ apply H2.
+ rewrite ass_app.
+ apply in3.
+ auto.
+ apply IHa.
+ rewrite <- ass_app.
+ rewrite <- ass_app in H.
+ rewrite <- app_comm_cons in H.
+ inversion H.
+ subst.
+ auto.
+ Qed.
+
+Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
+ induction x; intros.
+ simpl in H.
+ unfold stripOutVars.
+ simpl.
+ induction y; try destruct a; auto.
+ simpl.
+ rewrite IHy1.
+ rewrite IHy2.
+ reflexivity.
+ simpl in H.
+ apply distinct_app in H; destruct H; auto.
+ apply distinct_app in H; destruct H; auto.
+ rewrite <- app_comm_cons in H.
+ inversion H; subst.
+ set (IHx H3) as qq.
+ rewrite strip_lemma.
+ rewrite IHx.
+ apply notin_strip_inert.
+ unfold not; intros.
+ apply H2.
+ apply In_both'.
+ auto.
+ auto.
+ Qed.
+
+Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'.
+ intros.
+ induction y; auto.
+ simpl in H.
+ inversion H.
+ auto.
+ apply IHy.
+ simpl in H.
+ destruct (eqd_dec v a).
+ inversion H.
+ auto.
+ Qed.
+
+Lemma updating_stripped_tree_is_inert'
+ {Γ} lev
+ (ξ:VV -> LeveledHaskType Γ ★)
+ lv tree2 :
+ mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
+ = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
+
+ induction tree2.
+ destruct a; [ idtac | reflexivity ]; simpl.
+ induction lv; [ reflexivity | idtac ]; simpl.
+ destruct a; simpl.
+ set (eqd_dec v v0) as q; destruct q; auto.
+ set (dropVar (map (@fst _ _) lv) v) as b in *.
+ assert (dropVar (map (@fst _ _) lv) v=b). reflexivity.
+ destruct b; [ idtac | reflexivity ].
+ apply dropvar_lemma in H.
+ subst.
+ inversion IHlv.
+ rewrite H0.
+ clear H0 IHlv.
+ destruct (eqd_dec v0 v1).
+ subst.
+ assert False. apply n. intros; auto. inversion H.
+ reflexivity.
+ unfold stripOutVars in *.
+ simpl.
+ rewrite <- IHtree2_1.
+ rewrite <- IHtree2_2.
+ reflexivity.
+ Qed.
+
+Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False.
+ intros; induction a; auto.
+ simpl in H.
+ inversion H; subst.
+ apply H2; auto.
+ unfold In; simpl.
+ left; auto.
+ apply IHa.
+ clear IHa.
+ rewrite <- app_comm_cons in H.
+ inversion H; subst.
+ inversion H3; subst.
+ apply distinct_cons; auto.
+ intros.
+ apply H2.
+ simpl.
+ right; auto.
+ Qed.
+
+Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b).
+ intros.
+ apply distinct_cons.
+ induction b; intros; simpl; auto.
+ rewrite <- app_comm_cons in H.
+ inversion H; subst.
+ set (IHb H4) as H4'.
+ apply H4'.
+ inversion H0; subst; auto.
+ apply distinct_bogus in H; inversion H.
+ induction b; intros; simpl; auto.
+ apply distinct_nil.
+ apply distinct_app in H.
+ destruct H; auto.
+ Qed.
+
+Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b.
+ induction a; intros; simpl; auto.
+ rewrite <- app_comm_cons in H.
+ inversion H.
+ subst.
+ left; left; auto.
+ set (IHa _ _ H0) as H'.
+ destruct H'.
+ left; right; auto.
+ right; auto.
+ Qed.
+
+Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b).
+ intros.
+ induction a; simpl; auto.
+ simpl in H.
+ inversion H; auto.
+ assert (distinct (app a1 b)) as Q.
+ intros.
+ apply IHa.
+ clear IHa.
+ rewrite <- app_comm_cons in H.
+ inversion H; subst; auto.
+ apply distinct_cons; [ idtac | apply Q ].
+ intros.
+ apply in_both in H0.
+ destruct H0.
+ rewrite <- app_comm_cons in H.
+ inversion H; subst; auto.
+ apply H3.
+ apply In_both; auto.
+ rewrite <- app_comm_cons in H.
+ inversion H; subst; auto.
+ apply H3.
+ apply In_both'; auto.
+ simpl.
+ right; auto.
+ Qed.
+
+Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a).
+ induction a; intros; simpl; auto.
+ Qed.
+
+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_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+ forall v1 v2,
+ distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
+ mapOptionTree (update_xi ξ 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_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
+ distinct (map (@fst _ _) (leaves varstypes)) ->
+ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
+ mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+ set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q.
+ simpl in q.
+ rewrite <- app_nil_end in q.
+ apply q.
+ Qed.