---

Step * 1 of Lemma per-quotient-value-type


1. A : Type
2. E : A ⟶ A ⟶ ℙ
3. EquivRel(A;a,b.E[a;b])
4. value-type(A)
5. x : Base
6. x ∈ a,b:A/per/E[a;b]
7. v : a,b:A/per/E[a;b]
8. a,b:A/per/E[a;b] ⋂ Base ⊆r A
⊢ 0 ≤ eval v; 0
BY
{ (PointwiseFunctionality (-2)
   THEN (Assert a ∈ A BY
               (SubsumeC ⌜a,b:A/per/E[a;b] ⋂ Base⌝⋅ THEN Auto THEN Isect2CD THEN Auto))
   THEN (Assert b ∈ A BY
               (SubsumeC ⌜a,b:A/per/E[a;b] ⋂ Base⌝⋅ THEN Auto THEN Isect2CD THEN Auto))
   THEN RW (HigherC CallByValue2C) 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(A;a,b.E[a;b])
4.  value-type(A)
5.  x  :  Base
6.  x  \mmember{}  a,b:A/per/E[a;b]
7.  v  :  a,b:A/per/E[a;b]
8.  a,b:A/per/E[a;b]  \mcap{}  Base  \msubseteq{}r  A
\mvdash{}  0  \mleq{}  eval  v;  0


By

---

Latex:
(PointwiseFunctionality  (-2)
  THEN  (Assert  a  \mmember{}  A  BY
                          (SubsumeC  \mkleeneopen{}a,b:A/per/E[a;b]  \mcap{}  Base\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Isect2CD  THEN  Auto))
  THEN  (Assert  b  \mmember{}  A  BY
                          (SubsumeC  \mkleeneopen{}a,b:A/per/E[a;b]  \mcap{}  Base\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Isect2CD  THEN  Auto))
  THEN  RW  (HigherC  CallByValue2C)  0
  THEN  Auto)

---

Home Index