proposition: Lemma fv_closed_env : (forall rho, closed_env rho -> forall e, fv_exp e [<=] dom_rho rho -> fv_exp (nom_envsubst rho e) [=] {}).
proof: Proof. induction rho; intros; simpl in *. + fsetdec. + inversion H. eapply IHrho2; auto. rewrite fv_exp_subst_exp_upper. rewrite IHrho1; auto. fsetdec. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas