- [split
- [intros;apply (Hcut ? ? ? H2 ? H1 H3)
- |intros;apply (Hcut1 ? ? ? H3 ? ? ? ? ? ? H2 H4);reflexivity]
- |intros 9;cut (incl ? (fv_env (G2 @ ((mk_bound true X Q)::G1)))
- (fv_env (G2 @ ((mk_bound true X P)::G1))))
- [intros;
-(* [rewrite > H6 in H2;lapply (JS_to_WFT1 ? ? ? H8);
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H2 Hletin) *)
- generalize in match Hcut1;generalize in match H2;
- generalize in match H1;generalize in match H4;
- generalize in match G1;generalize in match G2;elim H1
- [apply SA_Top
- [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
- |rewrite > H9 in H6;apply (WFT_env_incl ? ? H6);elim l
- [simplify;unfold;intros;assumption
- |simplify;apply (incl_nat_cons ? ? ? H11)]]
- |apply SA_Refl_TVar
- [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
- |apply H10;rewrite < H9;assumption]
- |elim (decidable_eq_nat X n1)
- [apply (SA_Trans_TVar ? ? ? P)
- [rewrite < H12;elim l
- [simplify;apply in_Base
- |simplify;apply in_Skip;assumption]
- |lapply (JS_to_WFE ? ? ? H9);rewrite > H10 in Hletin;
- rewrite > H10 in H5;
- lapply (WFE_bound_bound ? ? ? Q ? Hletin H5)
- [lapply (H7 ? ? H8 H6 H10 H11);rewrite > Hletin1 in Hletin2;
- apply (Hcut ? ? ? ? ? H3 Hletin2);
- lapply (JS_to_WFE ? ? ? Hletin2);
- apply (JS_weakening ? ? ? H8 ? Hletin3);unfold;intros;
- elim l;simplify;apply in_Skip;assumption
- |rewrite > H12;elim l
- [simplify;apply in_Base
- |simplify;apply in_Skip;assumption]]]
- |rewrite > H10 in H5;apply (SA_Trans_TVar ? ? ? t1)
- [apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H5);unfold;
- intro;apply H12;symmetry;assumption
- |apply (H7 ? ? H8 H6 H10 H11)]]
- |apply SA_Arrow
- [apply (H6 ? ? H9 H5 H11 H12)
- |apply (H8 ? ? H9 H7 H11 H12)]
- |apply SA_All
- [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 s 0;simplify;intros;apply incl_nat_cons;assumption]]]
- |intros 4;(*generalize in match H1;*)elim H1
+ [intros;apply (Hcut1 ? ? ? H2 ? ? ? ? ? H3);reflexivity
+ |intros;cut (incl ? (fv_env (G2 @ ((mk_bound true X U)::G1)))
+ (fv_env (G2 @ ((mk_bound true X P)::G1))))
+ [intros;generalize in match H2;generalize in match Hcut1;
+ generalize in match Hcut;generalize in match G2;elim H1
+ [apply SA_Top
+ [rewrite > H8 in H4;lapply (JS_to_WFT1 ? ? ? H3);
+ apply (WFE_Typ_subst ? ? ? ? ? ? ? H4 Hletin)
+ |rewrite > H8 in H5;apply (WFT_env_incl ? ? H5 ? H7)]
+ |apply SA_Refl_TVar
+ [rewrite > H8 in H4;apply (WFE_Typ_subst ? ? ? ? ? ? ? H4);
+ apply (JS_to_WFT1 ? ? ? H3)
+ |rewrite > H8 in H5;apply (H7 ? H5)]
+ |elim (decidable_eq_nat X n)
+ [apply (SA_Trans_TVar ? ? ? P)
+ [rewrite < H10;elim l1
+ [simplify;constructor 1
+ |simplify;constructor 2;assumption]
+ |apply H7
+ [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin);
+ apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros;
+ elim l1;simplify;constructor 2;assumption
+ |lapply (WFE_bound_bound true n t1 U ? ? H4)
+ [apply (JS_to_WFE ? ? ? H5)
+ |rewrite < Hletin;apply (H6 ? H7 H8 H9)
+ |rewrite > H9;rewrite > H10;elim l1;simplify
+ [constructor 1
+ |constructor 2;assumption]]]]
+ |apply (SA_Trans_TVar ? ? ? t1)
+ [rewrite > H9 in H4;
+ apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4);
+ unfold;intro;apply H10;symmetry;assumption
+ |apply (H6 ? H7 H8 H9)]]
+ |apply SA_Arrow
+ [apply (H5 ? H8 H9 H10)
+ |apply (H7 ? H8 H9 H10)]
+ |apply SA_All
+ [apply (H5 ? H8 H9 H10)
+ |intros;apply (H7 ? ? (mk_bound true X1 t2::l1) H8)
+ [rewrite > H10;cut ((fv_env (l1@(mk_bound true X P::G1))) =
+ (fv_env (l1@(mk_bound true X U::G1))))
+ [unfold;intro;apply H11;rewrite > Hcut2;assumption
+ |elim l1
+ [simplify;reflexivity
+ |elim t4;simplify;rewrite > H12;reflexivity]]
+ |simplify;apply (incl_nat_cons ? ? ? H9)
+ |simplify;rewrite < H10;reflexivity]]]
+ |cut ((fv_env (G2@(mk_bound true X U::G1))) =
+ (fv_env (G2@(mk_bound true X P::G1))))
+ [rewrite > Hcut1;unfold;intros;assumption
+ |elim G2
+ [simplify;reflexivity
+ |elim t;simplify;rewrite > H4;reflexivity]]]]]
+ |intros 4;generalize in match H;elim H1