fact: Fixpoint aeq_f (n: nat) (L : atoms) (t1 : n_exp) (t2 : n_exp) : bool := match n with | 0 => false | S m => match t1 , t2 with | n_var x , n_var y => if (x == y) then true else false | n_abs x1 t1, n_abs x2 t2 => if (x1 == x2) then aeq_f m L t1 t2 else let (y,_) := atom_fresh L in aeq_f m ({{y}} \u L) (swap y x1 t1) (swap y x2 t2) | n_app t1 t2 , n_app t1' t2' => if aeq_f m L t1 t1' then aeq_f m L t2 t2' else false | _ , _ => false end end.
imports: Lia Metalib.Metatheory Metalib.LibLNgen