rewrite < Hletin2 in H12;rewrite < H14 in H12;lapply (H5 H12);
elim Hletin3]
|rewrite > subst_O_nat;apply in_FV_subst;assumption]]]
rewrite < Hletin2 in H12;rewrite < H14 in H12;lapply (H5 H12);
elim Hletin3]
|rewrite > subst_O_nat;apply in_FV_subst;assumption]]]