proposition: Lemma swap_spec : forall t w y, y `notin` fv_exp (nom_to_exp t) -> w <> y -> [w ~> var_f y] (nom_to_exp t) = nom_to_exp (swap w y t).
proof: Proof. intros. eapply swap_spec_aux with (t:=t)(m:=size t); auto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas