---

Step * of Lemma es-interface-map_wf

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[f:⋂es:EO+(Info). (A ⟶ E(X) ⟶ bag(B))].  (es-interface-map(f;X) ∈ EClass(B))
BY
{ WithCumulativity((Auto
                    THEN RepUR ``eclass es-interface-map let`` 0
                    THEN RepeatFor 2 ((MemCD THENA Auto))
                    THEN SplitOnConclITE
                    THEN Auto)) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. f : ⋂es:EO+(Info). (A ⟶ E(X) ⟶ bag(B))
6. es : EO+(Info)@i'
7. e : E@i
8. #(X es e) = 1 ∈ ℤ
⊢ single-valued-bag(X es e;A)

2
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. f : ⋂es:EO+(Info). (A ⟶ E(X) ⟶ bag(B))
6. es : EO+(Info)@i'
7. e : E@i
8. #(X es e) = 1 ∈ ℤ
⊢ e ∈ E(X)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[f:\mcap{}es:EO+(Info).  (A  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  bag(B))].
    (es-interface-map(f;X)  \mmember{}  EClass(B))


By

---

Latex:
WithCumulativity((Auto
                                    THEN  RepUR  ``eclass  es-interface-map  let``  0
                                    THEN  RepeatFor  2  ((MemCD  THENA  Auto))
                                    THEN  SplitOnConclITE
                                    THEN  Auto))

---

Home Index