proposition: Lemma aeq_nom_to_exp : forall n1 n2, aeq n1 n2 -> nom_to_exp n1 = nom_to_exp n2.
proof: Proof. induction 1; default_simp; autorewrite with lngen in *. - congruence. - rewrite (close_exp_wrt_exp_freshen y x); auto. rewrite swap_spec; auto. congruence. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas