| changeset 242 | 47de63a883c2 |
| parent 240 | 6cff34032a00 |
| child 245 | 55b156ac4a40 |
| 241:60acf3d3a4a0 | 242:47de63a883c2 |
|---|---|
76 fixes pi::"'x prm" |
76 fixes pi::"'x prm" |
77 shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)" |
77 shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)" |
78 sorry |
78 sorry |
79 |
79 |
80 lemma real_alpha: |
80 lemma real_alpha: |
81 assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s" |
81 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
82 shows "Lam a t = Lam b s" |
82 shows "Lam a t = Lam b s" |
83 sorry |
83 sorry |
84 |
84 |
85 |
85 |
86 |
86 |