---

Step * of Lemma eclass0-disjoint-classrel

∀[Info,A,B,C:Type]. ∀[Y:EClass(A)]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ bag(C)]. ∀[es:EO+(Info)].
  (disjoint-classrel(es;B;X;A;Y) ⇒ disjoint-classrel(es;C;(f o X);A;Y))
BY
{ ((At ⌈𝕌'⌉ Intros⋅ THEN Auto)
   THEN All(Unfold `disjoint-classrel`)
   THEN Auto
   THEN (InstHyp [⌈e⌉] (-2)⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN OrLeft
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN MaUseClassRel (-1)⋅
   THEN (Assert ¬b ∈ X(e) BY
               Auto)
   THEN Auto) }

---

Latex:


\mforall{}[Info,A,B,C:Type].  \mforall{}[Y:EClass(A)].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[es:EO+(Info)].
    (disjoint-classrel(es;B;X;A;Y)  {}\mRightarrow{}  disjoint-classrel(es;C;(f  o  X);A;Y))


By

((At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  Intros\mcdot{}  THEN  Auto)
  THEN  All(Unfold  `disjoint-classrel`)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  OrLeft
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  MaUseClassRel  (-1)\mcdot{}
  THEN  (Assert  \mneg{}b  \mmember{}  X(e)  BY
                          Auto)
  THEN  Auto)

---

Home Index