- |intros;apply (H7 ? ? (mk_bound true X1 t2::l) H8)
- [rewrite > H10;cut ((fv_env (l@(mk_bound true X P::G1))) =
- (fv_env (l@(mk_bound true X U::G1))))
- [unfold;intro;apply H11;unfold;rewrite > Hcut2;assumption
- |elim l
+ |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