Step * of Lemma rec-combined-class-opt-1-single-val

`∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(B)].`
`  (single-valued-classrel(es;lifting-2(F)|X,Prior(self)?init|;B)) supposing `
`     (single-valued-classrel(es;X;A) and `
`     (∀l:Id. single-valued-bag(init l;B)))`
BY
`{ ((UnivCD THENA Auto)`
`   THEN RepUR ``single-valued-classrel`` 0`
`   THEN Auto`
`   THEN InstLemma `rec-combined-class-opt-1-single-val0` [⌈Info⌉;⌈A⌉;⌈B⌉;⌈es⌉;⌈F⌉;⌈X⌉;⌈init⌉;⌈e⌉;⌈v1⌉;⌈v2⌉]⋅`
`   THEN Auto) }`

Latex:

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
(single-valued-classrel(es;lifting-2(F)|X,Prior(self)?init|;B))  supposing
(single-valued-classrel(es;X;A)  and
(\mforall{}l:Id.  single-valued-bag(init  l;B)))

By

Latex:
((UnivCD  THENA  Auto)
THEN  RepUR  ``single-valued-classrel``  0
THEN  Auto
THEN  InstLemma  `rec-combined-class-opt-1-single-val0`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};
\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}
THEN  Auto)

Home Index