---

Step * 1 of Lemma eclass0-single-val


1. Info : Type
2. B : Type
3. C : Type
4. X : EClass(B)
5. f : Id ─→ B ─→ bag(C)
6. es : EO+(Info)
7. ∀i:Id. ∀b:B.  single-valued-bag(f i b;C)
8. single-valued-classrel(es;X;B)
⊢ single-valued-classrel(es;(f o X);C)
BY
{ (UnfoldTopAb 0
   THEN Auto
   THEN All(MaUseClassRel)
   THEN All(BagMemberD)
   THEN SquashExRepD
   THEN All(RepUR ``class-ap``)
   THEN All(Fold `classrel`)
   THEN UseSingleVal (-5) (-2)
   THEN All(RepUR ``classrel``)
   THEN (InstHyp [⌈loc(e)⌉;⌈b⌉] (-12)⋅ THENA Auto)
   THEN UseSingleVal (-6) (-3))⋅ }

---

Latex:



1.  Info  :  Type
2.  B  :  Type
3.  C  :  Type
4.  X  :  EClass(B)
5.  f  :  Id  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)
6.  es  :  EO+(Info)
7.  \mforall{}i:Id.  \mforall{}b:B.    single-valued-bag(f  i  b;C)
8.  single-valued-classrel(es;X;B)
\mvdash{}  single-valued-classrel(es;(f  o  X);C)


By

(UnfoldTopAb  0
  THEN  Auto
  THEN  All(MaUseClassRel)
  THEN  All(BagMemberD)
  THEN  SquashExRepD
  THEN  All(RepUR  ``class-ap``)
  THEN  All(Fold  `classrel`)
  THEN  UseSingleVal  (-5)  (-2)
  THEN  All(RepUR  ``classrel``)
  THEN  (InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-12)\mcdot{}  THENA  Auto)
  THEN  UseSingleVal  (-6)  (-3))\mcdot{}

---

Home Index