proposition: Lemma fv_exp_open_exp_wrt_exp_upper : forall e1 e2, fv_exp (open_exp_wrt_exp e1 e2) [<=] fv_exp e2 `union` fv_exp e1.
proof: Proof. intros e1 e2. unfold open. generalize 0. induction e1; intro n0; simpl. - destruct (lt_eq_lt_dec n n0). destruct s. simpl. fsetdec. fsetdec. simpl. fsetdec. - fsetdec. - rewrite IHe1. fsetdec. - rewrite IHe1_1. rewrite IHe1_2. fsetdec. Qed.
imports: Metalib.Metatheory Stlc.Definitions String