---

Step * of Lemma provision-equality

No Annotations
∀[T:𝕌']. ∀[ok1,ok2:ℙ]. ∀[v1:⋂:↓ok1. T]. ∀[v2:⋂:↓ok2. T].
  (provision(ok1; v1) = provision(ok2; v2) ∈ Provisional(T)) supposing (((↓ok1) ⇒ (v1 = v2 ∈ T)) and (↓ok1 ⇐⇒ ↓ok2))
BY
{ (Auto
   THEN Unfold `provisional-type` 0
   THEN (QuotientEqTypeCDUp
         THENW (Auto
                THEN Unfold `provision` 0
                THEN (MemCD
                      THENL [Auto; (Unfold `uimplies` 0 THEN (MemTypeCD THENW Auto) THEN Unhide THEN Auto); Auto]
                ))
         )
   THEN RepUR ``provision`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}'].  \mforall{}[ok1,ok2:\mBbbP{}].  \mforall{}[v1:\mcap{}:\mdownarrow{}ok1.  T].  \mforall{}[v2:\mcap{}:\mdownarrow{}ok2.  T].
    (provision(ok1;  v1)  =  provision(ok2;  v2))  supposing  (((\mdownarrow{}ok1)  {}\mRightarrow{}  (v1  =  v2))  and  (\mdownarrow{}ok1  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}ok2))


By

---

Latex:
(Auto
  THEN  Unfold  `provisional-type`  0
  THEN  (QuotientEqTypeCDUp
              THENW  (Auto
                            THEN  Unfold  `provision`  0
                            THEN  (MemCD
                                        THENL  [Auto
                                                    ;  (Unfold  `uimplies`  0  THEN  (MemTypeCD  THENW  Auto)  THEN  Unhide  THEN  Auto)
                                                    ;  Auto]
                            ))
              )
  THEN  RepUR  ``provision``  0
  THEN  Auto)

---

Home Index