proposition: Lemma nom_to_exp_eq_aeq : forall n1 n2, nom_to_exp n1 = nom_to_exp n2 -> aeq n1 n2.
proof: Proof. induction n1; intro n2; destruct n2; default_simp. destruct (x == x0). - subst. eauto with lngen. - assert (FX : x `notin` fv_exp (nom_to_exp n2)). { intro IN. assert (x `in` fv_exp (nom_to_exp (n_abs x0 n2))). { simpl. autorewrite with lngen. fsetdec. } simpl in *. rewrite <- H0 in H. autorewrite with lngen in *. fsetdec. } eapply aeq_abs_diff; auto. + autorewrite with lngen. auto. + eapply IHn1. rewrite <- swap_spec; eauto. rewrite subst_exp_spec. rewrite <- H0. autorewrite with lngen. auto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas