131 definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx"

   132 

   133 lemma Lam_I : "\<II> = Lam[x]. Var x"

   134   by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)

   135      (metis Rep_name_inverse atom_name_def fresh_at_base)

   136 

   137 definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)"

   138 definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)"

   139 

   140 lemma c1_c2[simp]:

   141   "c1 \<noteq> c2"

   142   unfolding c1_def c2_def

   143   by (simp add: Abs_name_inject)

   144 

   145 definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2"

   146 lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y"

   147   by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)

   148      (metis Rep_name_inverse atom_name_def fresh_at_base)