fact: Fixpoint swap (x:atom) (y:atom) (t:n_exp) : n_exp := match t with | n_var z => n_var (swap_var x y z) | n_abs z t1 => n_abs (swap_var x y z) (swap x y t1) | n_app t1 t2 => n_app (swap x y t1) (swap x y t2) end.
imports: Lia Metalib.Metatheory Metalib.LibLNgen