- [intro;apply H13;apply H5;assumption
- |intro;apply H13;apply H5;apply (WFT_to_incl ? ? ? H3);
- assumption
- |simplify;autobatch
- |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
- [intros;apply H2
- [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;
- autobatch
- |apply (JS_weakening ? ? ? H9)
- [autobatch
- |unfold;intros;autobatch]
- |assumption]
- |*:autobatch]
- |autobatch]]]]]
+ [intro; autobatch;
+ |intro; apply H13;apply H5; apply (WFT_to_incl ? ? ? H3);
+ assumption
+ |simplify;autobatch
+ |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
+ [intros;apply H2
+ [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;
+ autobatch
+ |apply (JS_weakening ? ? ? H9)
+ [autobatch
+ |unfold;intros;autobatch]
+ |assumption]
+ |*:autobatch]
+ |autobatch]]]]]