proposition: Lemma aeq_equivariance : forall x y t1 t2, aeq t1 t2 -> aeq (swap x y t1) (swap x y t2).
proof: Proof. induction 1; intros; simpl in *; auto. destruct (swap_var x y x0 == swap_var x y y0). - rewrite e. eapply aeq_abs_same. rewrite swap_equivariance in IHaeq. rewrite e in IHaeq. rewrite swap_id in IHaeq. auto. - rewrite swap_equivariance in IHaeq. eapply aeq_abs_diff; auto. eapply notin_fv_nom_equivariance; auto. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen