proposition: Lemma in_fv_nom_equivariance : forall x y x0 t, x0 `in` fv_nom t -> swap_var x y x0 `in` fv_nom (swap x y t).
proof: Proof. induction t; intros; simpl in *. - unfold swap_var; default_simp; fsetdec. - unfold swap_var in *. default_simp; fsetdec. - destruct (AtomSetImpl.union_1 H); fsetdec. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen