---

Step * of Lemma disjoint-union-comb-disjoint-classrel

∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(C)].
  (disjoint-classrel(es;B;Y;C;Z) ⇒ disjoint-classrel(es;A;X;C;Z) ⇒ disjoint-classrel(es;A + B;X (+) Y;C;Z))
BY
{ ((UnivCD THENA Auto)
   THEN All (Unfold `disjoint-classrel`)⋅
   THEN Auto
   THEN RepeatFor 2 ((InstHyp [⌈e⌉] (-3)⋅ THENA Auto))
   THEN SplitOrHyps
   THEN Auto
   THEN OrLeft
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN MaUseClassRel (-1)
   THEN DVar `a'
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B,C:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(C)].
    (disjoint-classrel(es;B;Y;C;Z)
    {}\mRightarrow{}  disjoint-classrel(es;A;X;C;Z)
    {}\mRightarrow{}  disjoint-classrel(es;A  +  B;X  (+)  Y;C;Z))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All  (Unfold  `disjoint-classrel`)\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
  THEN  SplitOrHyps
  THEN  Auto
  THEN  OrLeft
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  MaUseClassRel  (-1)
  THEN  DVar  `a'
  THEN  All  Reduce
  THEN  Auto)

---

Home Index