proposition: Lemma subst_equivariance : forall u x y z t, swap x y (subst u z t) = subst (swap x y u) (swap_var x y z) (swap x y t).
proof: Proof. intros. eapply nominal_induction with (t := t). 2 : { intros. rewrite subst_abs. default_simp. rewrite subst_abs. default_simp. rewrite subst_abs. default_simp. rewrite <- e. Admitted. Lemma subst_same : forall t y, aeq (subst (n_var y) y t) t. Proof. intros t y. eapply nominal_induction with (t := t). - intros. destruct (x == y). subst. rewrite subst_eq_var. auto. rewrite subst_neq_var. auto. auto. - intros. rewrite subst_abs. destruct (y == x). eapply aeq_abs_same. eapply aeq_refl. destruct atom_fresh. simpl in n0. destruct (x0 == x). subst. rewrite swap_id. eapply aeq_abs_same. Admitted. Lemma aeq_fv_nom : forall t1 t2, aeq t1 t2 -> fv_nom t1 [=] fv_nom t2. Proof. induction 1; simpl in *; try fsetdec. unfold AtomSetImpl.Equal. intro a. rewrite remove_iff. rewrite remove_iff. rewrite IHaeq. clear IHaeq H1. split. + intros [K1 K2]. apply (in_fv_nom_equivariance y x) in K1. rewrite swap_involutive in K1. unfold swap_var in K1. destruct (a == y); subst. contradiction. destruct (a == x); subst. contradiction. split. auto. auto. + intros [K1 K2]. apply (in_fv_nom_equivariance y x) in K1. pose (J := notin_fv_nom_equivariance x y x t2 H0). clearbody J. unfold swap_var in *. default_simp. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen