---

Step * of Lemma parallel-class-loc-bounded

∀[T,Info:Type]. ∀[X,Y:EClass(T)].  (LocBounded(T;X) ⇒ LocBounded(T;Y) ⇒ LocBounded(T;X || Y))
BY
{ WithCumulativity(((UnivCD THENA Auto)
                    THEN D (-1)
                    THEN D (-3)
                    THEN RepUR ``loc-bounded-class class-loc-bound`` 0
                    THEN RepUR ``loc-bounded-class class-loc-bound`` (-1)
                    THEN RepUR ``loc-bounded-class class-loc-bound`` (-3)
                    THEN ExRepD
                    THEN InstConcl [⌜L1 + L⌝]⋅
                    THEN Auto
                    THEN MaUseClassRel (-1)
                    THEN D (-1)
                    THEN (Unhide THENA Auto)
                    THEN BagMemberD 0
                    THEN D 0
                    THEN D (-1)
                    THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[T,Info:Type].  \mforall{}[X,Y:EClass(T)].    (LocBounded(T;X)  {}\mRightarrow{}  LocBounded(T;Y)  {}\mRightarrow{}  LocBounded(T;X  ||  Y))


By

---

Latex:
WithCumulativity(((UnivCD  THENA  Auto)
                                    THEN  D  (-1)
                                    THEN  D  (-3)
                                    THEN  RepUR  ``loc-bounded-class  class-loc-bound``  0
                                    THEN  RepUR  ``loc-bounded-class  class-loc-bound``  (-1)
                                    THEN  RepUR  ``loc-bounded-class  class-loc-bound``  (-3)
                                    THEN  ExRepD
                                    THEN  InstConcl  [\mkleeneopen{}L1  +  L\mkleeneclose{}]\mcdot{}
                                    THEN  Auto
                                    THEN  MaUseClassRel  (-1)
                                    THEN  D  (-1)
                                    THEN  (Unhide  THENA  Auto)
                                    THEN  BagMemberD  0
                                    THEN  D  0
                                    THEN  D  (-1)
                                    THEN  Auto))

---

Home Index