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:
\mforall{}[T,Info:Type]. \mforall{}[X,Y:EClass(T)]. (LocBounded(T;X) {}\mRightarrow{} LocBounded(T;Y) {}\mRightarrow{} 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 [\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