---

Step * 1 of Lemma mset_mem_mon_for_union


1. s : DSet@i'
2. s' : DSet@i'
3. a : MSet{s}@i
4. e : |s| ⟶ MSet{s'}@i
5. x : |s'|@i
⊢ x ∈b msFor{<MSet{s'},⋃,0>} y ∈ a. e[y] = ∃b{s} y ∈ a. (x ∈b e[y])
BY
{ % Some proper HO matching would really be useful bere % 
 
RWH (LambdaC λz.(x
                ∈b z)) 0 }

1
1. s : DSet@i'
2. s' : DSet@i'
3. a : MSet{s}@i
4. e : |s| ⟶ MSet{s'}@i
5. x : |s'|@i
⊢ (λz.(x ∈b z)) (msFor{<MSet{s'},⋃,0>} y ∈ a. e[y]) = ∃b{s} y ∈ a. ((λz.(x ∈b z)) e[y])

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  s'  :  DSet@i'
3.  a  :  MSet\{s\}@i
4.  e  :  |s|  {}\mrightarrow{}  MSet\{s'\}@i
5.  x  :  |s'|@i
\mvdash{}  x  \mmember{}\msubb{}  msFor\{<MSet\{s'\},\mcup{},0>\}  y  \mmember{}  a.  e[y]  =  \mexists{}\msubb{}\{s\}  y  \mmember{}  a.  (x  \mmember{}\msubb{}  e[y])


By

---

Latex:
\%  Some  proper  HO  matching  would  really  be  useful  bere  \% 
 
RWH  (LambdaC  \mlambda{}z.(x
                                \mmember{}\msubb{}  z))  0

---

Home Index