proposition: Lemma notin_fv_nom_equivariance : forall x0 x y t , x0 `notin` fv_nom t -> swap_var x y x0 `notin` fv_nom (swap x y t).
proof: Proof. induction t; intros; simpl in *. - unfold swap_var; default_simp. - unfold swap_var in *. default_simp. - destruct_notin. eauto. Qed.
imports: Lia Metalib.Metatheory Metalib.LibLNgen