---

Step * of Lemma simple-comb-1-concat-classrel

∀[Info,B,C:Type]. ∀[f:B ⟶ bag(C)]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ f@|X|(e);↓∃b:B. (v ↓∈ f b ∧ b ∈ X(e)))
BY
{ (Unfold `concat-lifting-1` 0
   THEN Unfold `simple-comb-1` 0
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN (InstLemma `simple-comb1-concat-classrel` [⌜Info⌝; ⌜B⌝; ⌜C⌝; ⌜f⌝; ⌜X⌝; ⌜es⌝; ⌜e⌝; ⌜v⌝]⋅ THENA Auto)
   THEN Unfold `simple-comb1` (-1)
   THEN Auto
   THEN Try ((Using [`n',⌜1⌝;`A',⌜λn.[B][n]⌝] MemCD⋅ THEN MaAuto))
   THEN OnMaybeHyp 9 (\h. ((D h THEN Auto) THEN D 0 THEN ParallelLast THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[f:B  {}\mrightarrow{}  bag(C)].  \mforall{}[X:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:C].
    uiff(v  \mmember{}  f@|X|(e);\mdownarrow{}\mexists{}b:B.  (v  \mdownarrow{}\mmember{}  f  b  \mwedge{}  b  \mmember{}  X(e)))


By

---

Latex:
(Unfold  `concat-lifting-1`  0
  THEN  Unfold  `simple-comb-1`  0
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstLemma  `simple-comb1-concat-classrel`  [\mkleeneopen{}Info\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}C\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}X\mkleeneclose{};  \mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}v\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Unfold  `simple-comb1`  (-1)
  THEN  Auto
  THEN  Try  ((Using  [`n',\mkleeneopen{}1\mkleeneclose{};`A',\mkleeneopen{}\mlambda{}n.[B][n]\mkleeneclose{}]  MemCD\mcdot{}  THEN  MaAuto))
  THEN  OnMaybeHyp  9  (\mbackslash{}h.  ((D  h  THEN  Auto)  THEN  D  0  THEN  ParallelLast  THEN  Auto)))

---

Home Index