proposition: Lemma nom_envsubst_var : forall x rho e rho', closed_env rho -> Some (e,rho') = rho_lookup x rho -> nom_envsubst rho (var_f x) = nom_envsubst rho' (nom_to_exp e).
proof: Proof. induction rho. - intros. simpl in *. inversion H0. - intros. simpl in *. inversion H. subst. destruct (x == a). + inversion H0. subst. clear H0. simpl. rewrite (nom_envsubst_fresh_eq rho2); auto. apply fv_closed_env; auto. + eapply IHrho2; auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas