proposition: Lemma rho_lookup_closed_val : forall x rho e r, closed_env rho -> Some (e,r) = rho_lookup x rho -> fv_exp (nom_to_exp e) [<=] dom_rho r.
proof: Proof. induction rho; intros; simpl in *. - inversion H0. - inversion H. subst. destruct (x == a). inversion H0. eauto. eapply IHrho2; eauto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas