equal
deleted
inserted
replaced
57 by (rule eqvts) |
57 by (rule eqvts) |
58 |
58 |
59 term alpha_bi |
59 term alpha_bi |
60 |
60 |
61 lemma alpha_bi: |
61 lemma alpha_bi: |
62 shows "alpha_bi pi b b' = True" |
62 shows "alpha_bi b b' = True" |
63 apply(induct b rule: lam_bp_inducts(2)) |
63 apply(induct b rule: lam_bp_inducts(2)) |
64 apply(simp_all) |
64 apply(simp_all) |
65 apply(induct b' rule: lam_bp_inducts(2)) |
65 apply(induct b' rule: lam_bp_inducts(2)) |
66 apply (simp_all add: lam_bp_inject) |
66 apply (simp_all add: lam_bp_inject) |
67 done |
67 done |