+
+Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
+ induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
+Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
+ induction κ; auto. apply weakV; auto. Defined.
+Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
+ induction κ; auto. apply weakT; auto. Defined.
+Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
+ unfold HaskType in *.
+ unfold InstantiatedTypeEnv in *.
+ intros.
+ apply ilist_chop in X.
+ apply lt.
+ apply X.
+ Defined.
+Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
+ induction κ; auto. apply weakL; auto. Defined.
+Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
+ := match lt with t @@ l => weakT' t @@ weakL' l end.
+Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
+ induction κ; auto. apply weakCE; auto. Defined.
+Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
+ induction κ; auto.
+ apply weakCK.
+ apply IHκ.
+ Defined.
+Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
+ map weakCK' hck.
+
+Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ.
+ rewrite list_ins_app in ite.
+ set (weakITE' ite) as ite'.
+ set (ilist_chop ite) as a.
+ rewrite <- (list_take_drop _ Γ n).
+ apply ilist_app; auto.
+ inversion ite'; auto.
+ Defined.
+
+Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv.
+ unfold HaskTyVar; intros.
+ unfold HaskTyVar in cv'.
+ apply (cv' TV).
+ apply weakITE_ in env.
+ apply env.
+ Defined.
+
+Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂.
+ unfold HaskType; intros.
+ apply lt.
+ apply weakITE_ in X.
+ apply X.
+ Defined.
+Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ).
+ unfold HaskLevel; intros.
+ unfold HaskLevel in lev.
+ eapply map.
+ apply weakV_.
+ apply lev.
+ Defined.
+Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ :=
+ match lt with t@@l => weakT_ t @@ weakL_ l end.
+Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ).
+ unfold HaskCoercionKind; intros.
+ unfold HaskCoercionKind in hck.
+ apply hck.
+ apply weakITE_ in X.
+ apply X.
+ Defined.
+Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ.
+Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
+ forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂.
+ intros.
+ apply f.
+ apply weakITE_ in env.
+ apply env.
+ apply X.
+ Defined.
+Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ).
+ unfold HaskCoVar; intros.
+ unfold HaskCoVar in cv'.
+ apply (cv' TV).
+ apply weakITE_ in env.
+ apply env.
+ unfold InstantiatedCoercionEnv.
+ unfold InstantiatedCoercionEnv in cenv.
+ replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv.
+ apply cenv.
+ unfold weakCE_.
+ rewrite <- map_preserves_length.
+ reflexivity.
+ Defined.
+
+Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ.
+ intros.
+ unfold HaskTyVar.
+ intros.
+ rewrite list_ins_app in env.
+ apply weakITE' in env.
+ inversion env; subst; auto.
+ Defined.
+
+
+
+Fixpoint caseType0 {Γ}(lk:list Kind) :
+ IList _ (HaskType Γ) lk ->
+ HaskType Γ (fold_right KindArrow ★ lk) ->
+ HaskType Γ ★ :=
+ match lk as LK return
+ IList _ (HaskType Γ) LK ->
+ HaskType Γ (fold_right KindArrow ★ LK) ->
+ HaskType Γ ★
+ with
+ | nil => fun _ ht => ht
+ | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
+ end.
+
+Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
+ caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
+