Step * of Lemma simple-loc-comb-2-loc-bounded3

[Info,A,B,C:Type]. ∀[f:Id ─→ A ─→ B ─→ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (LocBounded(B;Y)  LocBounded(C;lifting-loc-2(f) (Loc,X, Y)))
BY
((UnivCD THENA Auto)
   THEN RepUR ``loc-bounded-class class-loc-bound`` 0
   THEN RepUR ``loc-bounded-class class-loc-bound`` (-1)
   THEN (-1)
   THEN ExRepD
   THEN InstConcl [⌈L⌉]⋅
   THEN Auto
   THEN MaUseClassRel (-1)
   THEN (-1)
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN InstHyp [⌈es⌉; ⌈b⌉; ⌈e⌉(-9)⋅
   THEN Auto)⋅ }


Latex:



Latex:
\mforall{}[Info,A,B,C:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (LocBounded(B;Y)  {}\mRightarrow{}  LocBounded(C;lifting-loc-2(f)  o  (Loc,X,  Y)))


By


Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``loc-bounded-class  class-loc-bound``  0
  THEN  RepUR  ``loc-bounded-class  class-loc-bound``  (-1)
  THEN  D  (-1)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  MaUseClassRel  (-1)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}]  (-9)\mcdot{}
  THEN  Auto)\mcdot{}




Home Index