proposition: Lemma nom_envsubst_open : forall rho e e', (forall v, lc_exp (nom_val_to_exp v)) -> (nom_envsubst rho (open e e')) = (open (nom_envsubst rho e) (nom_envsubst rho e')).
proof: Proof. induction rho; intros; default_simp. rewrite subst_exp_open_exp_wrt_exp; eauto. admit. Admitted. Lemma nom_envsubst_fresh_eq : forall rho e, closed_env rho -> fv_exp e [=] {} -> nom_envsubst rho e = e. Proof. induction rho. simpl. auto. intros. simpl. inversion H. rewrite subst_exp_fresh_eq; auto. rewrite H0. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas