33   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"

    33   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"

    34   by simp

    34   by simp

    35 

    35 

    36 lemma bi_eqvt:

    36 lemma bi_eqvt:

    37   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"

    37   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"

    45 

    39 

    46 lemma supp_fv:

    40 lemma supp_fv:

    47   "supp t = fv_lam t" and 

    41   "supp t = fv_lam t" and 

    48   "supp b = fv_bp b"

    42   "supp b = fv_bp b"

    49 apply(induct t and b rule: lam_bp_inducts)

    43 apply(induct t and b rule: lam_bp_inducts)