608 text {* TODO: nominal_primrec throws RSN if an argument is not in FS, but function works *}

   609 function q where

   610   "q (Lam [x]. M) N = Lam [x]. (Lam [x]. (App M (q (Var x) N)))"

   611 | "q (Var x) N = Var x"

   612 | "q (App l r) N = App l r"

   613 oops

   614 

   615 text {* TODO: eqvt_at for the other side *}

   616 nominal_primrec q where

   617   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"

   618 | "q (Var x) N = Var x"

   619 | "q (App l r) N = App l r"

   620 unfolding eqvt_def q_graph_def

   621 apply (rule, perm_simp, rule)

   622 apply (rule TrueI)

   623 apply (case_tac x)

   624 apply (rule_tac y="a" in lam.exhaust)

   625 apply simp_all

   626 apply blast

   627 apply blast

   628 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)

   629 apply blast

   630 apply clarify

   631 apply (rule_tac x="(x, xa, M, Ma, c, ca, Na)" and ?'a="name" in obtain_fresh)

   632 apply (subgoal_tac "eqvt_at q_sumC (Var ca, Na)") --"Could come from nominal_function?"

   633 apply (subgoal_tac "Lam [c]. App M (q_sumC (Var c, Na)) = Lam [a]. App M (q_sumC (Var a, Na))")

   634 apply (subgoal_tac "Lam [ca]. App Ma (q_sumC (Var ca, Na)) = Lam [a]. App Ma (q_sumC (Var a, Na))")

   635 apply (simp only:)

   636 apply (erule Abs_lst1_fcb)

   637 oops

   638