proposition: Lemma aeq_sym : forall t1 t2, aeq t1 t2 -> aeq t2 t1.
proof: Proof. induction 1; auto. - eapply aeq_abs_diff; auto. rewrite aeq_fv_nom; eauto. pose (J := notin_fv_nom_equivariance x y x t2 H0). clearbody J. unfold swap_var in J. default_simp. eapply aeq_equivariance in IHaeq. rewrite swap_involutive in IHaeq. rewrite swap_symmetric. auto. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen