546   shows "(supp (Var a)) = {a:::name}"

   546   shows "(supp (Var a)) = {a:::name}"

   547   using var_supp1 by (simp add: supp_at_base)

   547   using var_supp1 by (simp add: supp_at_base)

   548 

   548 

   549 lemma app_supp:

   549 lemma app_supp:

   550   shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"

   550   shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)"

   552 apply(simp add: Collect_imp_eq Collect_neg_eq)

   552 apply(simp add: Collect_imp_eq Collect_neg_eq)

   553 done

   553 done

   554 

   554 

   555 (* supp for lam *)

   555 (* supp for lam *)

   556 lemma lam_supp1:

   556 lemma lam_supp1: