---

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