| changeset 245 | 55b156ac4a40 |
| parent 243 | 22715cab3995 |
| parent 242 | 47de63a883c2 |
| child 246 | 6da7d538e5e0 |
| 244:42dac1cfcd14 | 245:55b156ac4a40 |
|---|---|
107 lemma fv_lam: |
107 lemma fv_lam: |
108 shows "fv (Lam a t) = (fv t) - {a}" |
108 shows "fv (Lam a t) = (fv t) - {a}" |
109 sorry |
109 sorry |
110 |
110 |
111 lemma real_alpha: |
111 lemma real_alpha: |
112 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>[b].s" |
112 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
113 shows "Lam a t = Lam b s" |
113 shows "Lam a t = Lam b s" |
114 sorry |
114 sorry |
115 |
115 |
116 |
116 |
117 |
117 |