proposition: Lemma swap_spec_aux : forall m t w y, size t <= m -> y `notin` fv_exp (nom_to_exp t) -> w <> y -> [w ~> var_f y] (nom_to_exp t) = nom_to_exp (swap w y t).
proof: Proof. induction m; intros t w y SZ; destruct t; simpl in *; try lia; intros. + unfold swap_var; default_simp. + unfold swap_var; default_simp. { rewrite subst_exp_fresh_eq; default_simp. autorewrite with lngen in *. rewrite (close_exp_wrt_exp_freshen w y); try fsetdec. rewrite IHm; default_simp. } { autorewrite with lngen in *. pick fresh z for ( fv_exp (nom_to_exp t) \u fv_exp (nom_to_exp (swap w y t)) \u {{w}} \u {{y}}). rewrite (close_exp_wrt_exp_freshen y z); auto. rewrite (close_exp_wrt_exp_freshen w z); auto. rewrite subst_exp_close_exp_wrt_exp; auto. rewrite IHm with (y:=z); default_steps. rewrite IHm with (y:=z); default_steps. rewrite IHm with (y:=y); default_steps. rewrite shuffle_swap; auto. rewrite <- fv_nom_fv_exp_eq. apply fv_nom_swap. rewrite fv_nom_fv_exp_eq. fsetdec. } { rewrite <- IHm; default_steps. autorewrite with lngen in *. fsetdec. } + rewrite IHm; auto; try lia; try fsetdec. rewrite IHm; auto; try lia; try fsetdec. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas