proposition: Lemma subst_exp_fresh_eq : forall (x : var) e u, x `notin` fv_exp e -> [x ~> u] e = e.
proof: Proof. intros x e u H. induction e. - Case "var_b". auto. - Case "var_f". simpl. destruct (x0 == x). + SCase "x0=x". subst. simpl fv_exp in H. fsetdec. + SCase "x0<>x". auto. - Case "abs". simpl. f_equal. auto. - Case "app". simpl in *. f_equal. auto. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions String