proposition: Lemma fv_exp_subst_exp_notin : forall x y u e, x `notin` fv_exp e -> x `notin` fv_exp u -> x `notin` fv_exp ([y ~> u]e).
proof: Proof. intros x y u e Fr1 Fr2. induction e; simpl in *. - Case "var_b". assumption. - Case "var_f". destruct (x0 == y). assumption. simpl. assumption. - Case "abs". apply IHe. assumption. - Case "app". destruct_notin. apply notin_union. apply IHe1. assumption. apply IHe2. assumption. Qed.
imports: Metalib.Metatheory Stlc.Definitions String