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