---

Step * of Lemma simple-comb-2-es-sv

∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[F:A ⟶ B ⟶ C]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (es-sv-class(es;lifting-2(F)|X, Y|)) supposing (es-sv-class(es;Y) and es-sv-class(es;X))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `simple-comb-2` 0
   THEN (Using [`A',⌜λn.[A; B][n]⌝;`n',⌜2⌝;`B',⌜C⌝] (BLemma `simple-comb-es-sv`)⋅
         THENA (Try (((MemCD THENA Auto) THEN IntSegCases (-1) THEN Reduce 0 THEN Auto)) THEN Auto)
         )
   THEN Reduce 0
   THEN Auto
   THEN Try ((IntSegCases (-1) THEN Reduce 0 THEN Hypothesis))) }

1
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. es : EO+(Info)
6. F : A ⟶ B ⟶ C
7. X : EClass(A)
8. Y : EClass(B)
9. es-sv-class(es;X)
10. es-sv-class(es;Y)
11. bs : k:ℕ2 ⟶ bag([A; B][k])@i
12. ∀k:ℕ2. (#(bs k) ≤ 1)@i
⊢ #(lifting-2(F) (bs 0) (bs 1)) ≤ 1

---

Latex:

---

Latex:
\mforall{}[Info,A,B,C:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (es-sv-class(es;lifting-2(F)|X,  Y|))  supposing  (es-sv-class(es;Y)  and  es-sv-class(es;X))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `simple-comb-2`  0
  THEN  (Using  [`A',\mkleeneopen{}\mlambda{}n.[A;  B][n]\mkleeneclose{};`n',\mkleeneopen{}2\mkleeneclose{};`B',\mkleeneopen{}C\mkleeneclose{}]  (BLemma  `simple-comb-es-sv`)\mcdot{}
              THENA  (Try  (((MemCD  THENA  Auto)  THEN  IntSegCases  (-1)  THEN  Reduce  0  THEN  Auto))  THEN  Auto)
              )
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((IntSegCases  (-1)  THEN  Reduce  0  THEN  Hypothesis)))

---

Home Index