- [apply SA_Top
- [rewrite > H5 in H3;
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H3 (JS_to_WFT1 ? ? ? H))
- |rewrite > H5 in H4;apply (WFT_env_incl ? ? H4);apply incl_fv_env]
- |apply SA_Refl_TVar
- [rewrite > H5 in H3;apply (WFE_Typ_subst ? ? ? ? ? ? ? H3);
- apply (JS_to_WFT1 ? ? ? H)
- |rewrite > H5 in H4;rewrite < fv_env_extends;apply H4]
+ [letin x \def fv_env. letin y ≝incl.
+ (* autobatch depth=4 size=8 by SA_Top, WFE_Typ_subst, H3, JS_to_WFT1, H, H4, WFT_env_incl, incl_fv_env]*)
+ apply SA_Top
+ [autobatch by WFE_Typ_subst, H3, JS_to_WFT1, H.
+ (*
+ rewrite > H5 in H3;
+ apply (WFE_Typ_subst ? ? ? ? ? ? ? H3 (JS_to_WFT1 ? ? ? H)) *)
+ |autobatch by H4, WFT_env_incl, incl_fv_env]
+ (* rewrite > H5 in H4;apply (WFT_env_incl ? ? H4);apply incl_fv_env] *)
+ |autobatch depth=4 by SA_Refl_TVar, WFE_Typ_subst, H3, JS_to_WFT1, H, H4.
+ (*
+ apply SA_Refl_TVar;
+ [autobatch by WFE_Typ_subst, H3, JS_to_WFT1, H.
+ (*
+ rewrite > H5 in H3;apply (WFE_Typ_subst ? ? ? ? ? ? ? H3);
+ apply (JS_to_WFT1 ? ? ? H) *)
+ |autobatch by H4. (* rewrite > H5 in H4;rewrite < fv_env_extends;apply H4*)] *)