---

Step * of Lemma simple-comb-1-classrel

∀[Info,B,C:Type]. ∀[f:B ⟶ C]. ∀[X:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:C].
  uiff(v ∈ lifting-1(f)|X|(e);↓∃b:B. ((v = (f b) ∈ C) ∧ b ∈ X(e)))
BY
{ (Unfold `lifting-1` 0
   THEN Unfold `simple-comb-1` 0
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN (InstLemma `simple-comb1-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))) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `lifting-1`  0
  THEN  Unfold  `simple-comb-1`  0
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstLemma  `simple-comb1-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)))

---

Home Index