---

Step * of Lemma quotient-value-type

∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (value-type(a,b:A//E[a;b])) supposing (value-type(A) and EquivRel(A;a,b.E[a;b]))
BY
{ ((ValueTypeAuto THEN (Assert a,b:A//E[a;b] ⋂ Base ⊆r A BY (RWO "quotient-isect-base" 0⋅ THEN Auto)))
   THEN PointwiseFunctionality (-2)
   THEN RW (HigherC CallByValue2C) 0
   THEN Auto
   THEN ((Assert ⌜a ∈ A⌝⋅ THEN Auto THEN SubsumeC ⌜a,b:A//E[a;b] ⋂ Base⌝⋅ THEN Auto THEN Isect2CD THEN Auto)⋅
   ORELSE (Assert ⌜b ∈ A⌝⋅ THEN Auto THEN SubsumeC ⌜a,b:A//E[a;b] ⋂ Base⌝⋅ THEN Auto THEN Isect2CD THEN Auto)⋅
   )) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (value-type(a,b:A//E[a;b]))  supposing  (value-type(A)  and  EquivRel(A;a,b.E[a;b]))


By

---

Latex:
((ValueTypeAuto  THEN  (Assert  a,b:A//E[a;b]  \mcap{}  Base  \msubseteq{}r  A  BY  (RWO  "quotient-isect-base"  0\mcdot{}  THEN  Auto)))
  THEN  PointwiseFunctionality  (-2)
  THEN  RW  (HigherC  CallByValue2C)  0
  THEN  Auto
  THEN  ((Assert  \mkleeneopen{}a  \mmember{}  A\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  SubsumeC  \mkleeneopen{}a,b:A//E[a;b]  \mcap{}  Base\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  Isect2CD
                THEN  Auto)\mcdot{}
  ORELSE  (Assert  \mkleeneopen{}b  \mmember{}  A\mkleeneclose{}\mcdot{}
                  THEN  Auto
                  THEN  SubsumeC  \mkleeneopen{}a,b:A//E[a;b]  \mcap{}  Base\mkleeneclose{}\mcdot{}
                  THEN  Auto
                  THEN  Isect2CD
                  THEN  Auto)\mcdot{}
  ))

---

Home Index