- [apply (H6 ? ? H9 H5 H11 H12)
- |intros;apply (H8 ? ? (mk_bound true X1 t2::l) l1)
- [unfold;intro;apply H13;rewrite > H11 in H14;apply (H12 ? H14)
- |assumption
- |apply H7;rewrite > H11;unfold;intro;apply H13;apply (H12 ? H14)
- |simplify;rewrite < H11;reflexivity
- |simplify;apply incl_nat_cons;assumption]]]
- |elim G2 0
- [simplify;unfold;intros;assumption
- |intro;elim t 0;simplify;intros;apply incl_nat_cons;assumption]]]
- |intros 4;(*generalize in match H1;*)elim H1
- [inversion H5
- [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
- |intros;destruct H9
- |intros;destruct H10
- |*:intros;destruct H11]
- |assumption
- |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 ? H5 H6)
- |inversion H7
- [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow
- [apply (JS_to_WFT2 ? ? ? H2)
- |apply (JS_to_WFT1 ? ? ? H4)]
- |intros;destruct H11
- |intros;destruct H12
- |intros;destruct H13;elim (H (pred m))
- [apply SA_Arrow
- [rewrite > H12 in H2;rewrite < Hcut in H8;
- apply (H15 ? ? ? ? ? H8 H2);lapply (t_len_arrow1 t2 t3);
- unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
- apply (t_len_pred ? ? Hletin1)
- |rewrite > H12 in H4;rewrite < Hcut1 in H10;
- apply (H15 ? ? ? ? ? H4 H10);lapply (t_len_arrow2 t2 t3);
- unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
- apply (t_len_pred ? ? Hletin1)]
- |apply (pred_m_lt_m ? ? H6)]
- |intros;destruct H13]
- |inversion H7
- [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall
- [apply (JS_to_WFT2 ? ? ? H2)
- |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin);
- apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros;
- assumption]
- |intros;destruct H11
- |intros;destruct H12
- |intros;destruct H13
- |intros;destruct H13;elim (H (pred m))
- [elim (fresh_name ((fv_env e1) @ (fv_type t1) @ (fv_type t7)));
- cut ((\lnot (in_list ? a (fv_env e1))) \land
- (\lnot (in_list ? a (fv_type t1))) \land
- (\lnot (in_list ? a (fv_type t7))))
- [elim Hcut2;elim H18;clear Hcut2 H18;apply (SA_All2 ? ? ? ? ? a)
- [rewrite < Hcut in H8;rewrite > H12 in H2;
- apply (H15 ? ? ? ? ? H8 H2);lapply (t_len_forall1 t2 t3);
- unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
- apply (t_len_pred ? ? Hletin1)
- |5:lapply (H10 ? H20);rewrite > H12 in H5;
- lapply (H5 ? H20 (subst_type_O t5 (TFree a)))
- [apply (H15 ? ? ? ? ? ? Hletin)
- [rewrite < Hcut1;rewrite > subst_O_nat;
- rewrite < eq_t_len_TFree_subst;
- lapply (t_len_forall2 t2 t3);unfold in Hletin2;
- lapply (trans_le ? ? ? Hletin2 H6);
- apply (t_len_pred ? ? Hletin3)
- |rewrite < Hcut in H8;
- apply (H16 e1 (nil ?) a t6 t2 ? ? ? Hletin1 H8);
- lapply (t_len_forall1 t2 t3);unfold in Hletin2;
- lapply (trans_le ? ? ? Hletin2 H6);
- apply (t_len_pred ? ? Hletin3)]
- |rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
- lapply (t_len_forall2 t2 t3);unfold in Hletin1;
- lapply (trans_le ? ? ? Hletin1 H6);
- apply (trans_le ? ? ? ? Hletin2);constructor 2;
- constructor 1
- |rewrite > Hcut1;rewrite > H12 in H4;
- lapply (H4 ? H20);rewrite < Hcut1;apply JS_Refl
- [apply (JS_to_WFT2 ? ? ? Hletin1)
- |apply (JS_to_WFE ? ? ? Hletin1)]]
- |*:assumption]
- |split
- [split
- [unfold;intro;apply H17;
- apply (natinG_or_inH_to_natinGH ? (fv_env e1));right;
- assumption
- |unfold;intro;apply H17;
- apply (natinG_or_inH_to_natinGH
- ((fv_type t1) @ (fv_type t7)));left;
- apply natinG_or_inH_to_natinGH;right;assumption]
- |unfold;intro;apply H17;
- apply (natinG_or_inH_to_natinGH
- ((fv_type t1) @ (fv_type t7)));left;
- apply natinG_or_inH_to_natinGH;left;assumption]]
- |apply (pred_m_lt_m ? ? H6)]]]]