Step * of Lemma classfun-res-disjoint-union-comb-left

`∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].`
`  (X (+) Y@e = (inl X@e) ∈ (A + B)) supposing `
`     (single-valued-classrel(es;X;A) and `
`     disjoint-classrel(es;A;X;B;Y) and `
`     (↑e ∈b X))`
BY
`{ ((UnivCD THENA Auto)`
`   THEN RepUR ``disjoint-union-comb`` 0`
`   THEN (InstLemma `classfun-res-parallel-class-left` [⌈Info⌉;⌈A + B⌉;⌈es⌉;⌈lifting-1(λx.(inl x))|X|⌉;`
`         ⌈lifting-1(λx.(inr x ))|Y|⌉;⌈e⌉]⋅`
`         THENA Auto`
`         )`
`   THEN Try (Complete (DisjointClassRel))) }`

1
`.....antecedent..... `
`1. Info : Type`
`2. A : Type`
`3. B : Type`
`4. es : EO+(Info)`
`5. X : EClass(A)`
`6. Y : EClass(B)`
`7. e : E`
`8. ↑e ∈b X`
`9. disjoint-classrel(es;A;X;B;Y)`
`10. single-valued-classrel(es;X;A)`
`⊢ ↑e ∈b lifting-1(λx.(inl x))|X|`

2
`1. Info : Type`
`2. A : Type`
`3. B : Type`
`4. es : EO+(Info)`
`5. X : EClass(A)`
`6. Y : EClass(B)`
`7. e : E`
`8. ↑e ∈b X`
`9. disjoint-classrel(es;A;X;B;Y)`
`10. single-valued-classrel(es;X;A)`
`11. lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e ~ lifting-1(λx.(inl x))|X|@e`
`⊢ lifting-1(λx.(inl x))|X| || lifting-1(λx.(inr x ))|Y|@e = (inl X@e) ∈ (A + B)`

Latex:

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[e:E].
(X  (+)  Y@e  =  (inl  X@e))  supposing
(single-valued-classrel(es;X;A)  and
disjoint-classrel(es;A;X;B;Y)  and
(\muparrow{}e  \mmember{}\msubb{}  X))

By

Latex:
((UnivCD  THENA  Auto)
THEN  RepUR  ``disjoint-union-comb``  0
THEN  (InstLemma  `classfun-res-parallel-class-left`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A  +  B\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}lifting-1(\mlambda{}x.(inl  x))|X|\mkleeneclose{};
\mkleeneopen{}lifting-1(\mlambda{}x.(inr  x  ))|Y|\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
THENA  Auto
)
THEN  Try  (Complete  (DisjointClassRel)))

Home Index