.
      eapply stp2_refl. eapply closed_upgrade_free. eassumption. omega.

      destruct H3. destruct H3. subst. simpl.
      inversion H3. omega. (* contra *)

      destruct H3. destruct H3. eauto. (* contra *)

      (* --- *)

      destruct H0. destruct H0. subst. simpl.
      destruct H3. destruct H0. subst. simpl.
      eapply stpd2_sel2. eauto. eauto.
      eapply stpd2_wrapf.
      eapply stp2_refl. eapply closed_upgrade_free. eassumption. omega.

      destruct H0. destruct H0. inversion H0. omega. (* contra *)

      destruct H0. destruct H0. eauto. (* contra *)

      (* --- *)

      destruct H0. destruct H0. subst. simpl.
      destruct H3. destruct H0. subst. simpl.
      eapply stp2_refl. eapply closed_upgrade_free. eassumption. omega.

      destruct H0. destruct H0. inversion H0. omega.
      destruct H0. destruct H0. eauto.
      destruct H0. destruct H0. inversion H0. omega.
      destruct H0. destruct H0. eauto.

    + destruct H3. destruct H3. omega.
    + destruct H2. destruct H3. omega.
    + destruct H2. destruct H2. destruct H4. destruct H5.
      destruct H3. destruct H3. destruct H7. destruct H8.
      subst. eapply stpd2_selax. eauto.

    + eauto.
    + subst GH. eauto.
    + eauto.
    + eauto.
    + eauto. subst GH. eauto.
    + eauto.

  - Case "all".
    intros GH0 GH0' GX TX T1' T2'? CX IX1 IX2 FA; eapply stpd2_wrapf.

    assert (length GH = length GH0 + 1). subst GH. eapply app_length.
    assert (length GH0 = length GH0') as EL. eapply Forall2_length. eauto.

    eapply compat_all in IX1. repeat destruct IX1 as [? IX1].
    eapply compat_all in IX2. repeat destruct IX2 as [? IX2].

    subst.

    eapply stpd2_all.
    + eapply IHn; eauto; try omega.
    + eauto.
    + eauto.
    + eauto.
    + subst.
      eapply IHn. eauto. omega. simpl.
      change ((G2, T3) :: GH0 ++ [(GX, TX)]) with (((G2, T3) :: GH0) ++ [(GX, TX)]).
      reflexivity.
      eauto.
      rewrite app_length. simpl. rewrite EL. eauto.
      rewrite app_length. simpl. rewrite EL. eauto.
      eapply Forall2_cons. simpl. eauto. eauto.
    + eauto.
    + eauto. subst GH. rewrite <-EL. eapply closed_upgrade_free. eauto. omega.
    + eauto.
    + eauto. subst GH. rewrite <-EL. eapply closed_upgrade_free. eauto. omega.
  - Case "wrapf".
    intros. subst. eapply IHn; eauto; try omega.
  - Case "transf".
    intros. subst.
    apply stp2_extend2 with (v1:=(vty GX TX)) in H.
    apply stp2_extend1 with (v1:=(vty GX TX)) in H0.
    eapply stpd2_trans.

    eapply IHn; eauto; try omega.
    unfold compat. simpl. left. exists (length G2).
    rewrite <- beq_nat_refl. split; eauto.

    eapply IHn; eauto; try omega.
    unfold compat. simpl. left. exists (length G2).
    rewrite <- beq_nat_refl. split; eauto.
Qed.

Lemma stp2_substitute: forall G1 G2 T1 T2 GH m,
   stpd2 m G1 T1 G2 T2 GH ->
   forall GH0 GH0' GX TX T1' T2',
     GH = (GH0 ++ [(GX, TX)]) ->
     closed 0 0 (length GX) TX ->
     compat GX TX G1 T1 T1' ->
     compat GX TX G2 T2 T2' ->
     Forall2 (compat2 GX TX) GH0 GH0' ->
     stpd2 false G1 T1' G2 T2' GH0'.
Proof.
  intros. repeat eu. eapply stp2_substitute_aux; eauto.
Qed.

(* ### Relating Static and Dynamic Subtyping ### *)
Lemma stp_to_stp2: forall G1 GH T1 T2,
  stp G1 GH T1 T2 ->
  forall GX GY, wf_env GX G1 -> wf_envh GX GY GH ->
  stpd2 false GX T1 GX T2 GY.
Proof.
  intros G1 G2 T1 T2 ST. induction ST; intros GX GY WX WY; eapply stpd2_wrapf.
  - Case "top".
    eapply stpd2_top. erewrite wfh_length; eauto. erewrite wf_length; eauto.
  - Case "fun". eapply stpd2_fun; eauto.
  - Case "sel1".
    assert (exists v : vl, indexr x GX = Some v /\ val_type GX v (bind_ty T)) as A.
    eapply indexr_safe_ex. eauto. eauto.
    destruct A as [? [? VT]].
    inversion VT; subst.
    destruct H6 as [? H6].
    eapply stpd2_sel1; eauto.
    eapply stp2_closed1 in H6. simpl in H6. eauto.
    eapply stpd2_trans.
    eexists. eapply stp2_wrapf. apply stp2_extendH_mult with (H2:=GY) in H6. rewrite app_nil_r in H6. eapply H6.
    eapply IHST. eauto. eauto.
  - Case "selx". eauto.
    assert (exists v0 : vl, indexr x GX = Some v0 /\ val_type GX v0 v) as A.
    eapply indexr_safe_ex. eauto. eauto. eauto.
    destruct A as [? [??]].
    eapply stpd2_selx; eauto.
  - Case "sela1". eauto.
    assert (exists v, indexr x GY = Some v /\ valh_type GX GY v (bind_ty T)) as A.
    eapply index_safeh_ex. eauto. eauto. eauto.
    destruct A as [? [? VT]]. destruct x0.
    inversion VT. subst.
    eapply stpd2_sela1. eauto.
    erewrite wf_length; eauto.
    eapply IHST. eauto. eauto.
  - Case "selax". eauto.
    assert (exists v0, indexr x GY = Some v0 /\ valh_type GX GY v0 v) as A.
    eapply index_safeh_ex. eauto. eauto. eauto.
    destruct A as [? [? VT]]. destruct x0.
    destruct VT. subst.
    eapply stpd2_selax. eauto.
  - Case "all".
    subst x.
    assert (length GY = length GH) as A. eapply wfh_length; eauto.
    assert (length GX = length G1) as B. eapply wf_length; eauto.
    eapply stpd2_all. eauto. eauto.
    rewrite A. rewrite B. eauto.
    rewrite A. rewrite B. eauto.
    rewrite A.
    eapply IHST2. eauto. eapply wfeh_cons. eauto.
Qed.

Lemma valtp_widen: for