---

Step * of Lemma eo_record_cumulative

eo_record{i:l}() ⊆r eo_record{j:l} supposing Type ⊆r 𝕌{j}
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D (-1)
   THEN Try ((Unfold `eo_record` 0
              THEN (Assert x ∈ Atom ─→ Top BY
                          (RepUR ``record`` 3 THEN Auto))
              THEN Repeat ( RecordPlusTypeCD THENL [Id; Auto]))⋅)
   THEN Auto) }

---

Latex:


eo\_record\{i:l\}()  \msubseteq{}r  eo\_record\{j:l\}  supposing  Type  \msubseteq{}r  \mBbbU{}\{j\}


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  (-1)
  THEN  Try  ((Unfold  `eo\_record`  0
                        THEN  (Assert  x  \mmember{}  Atom  {}\mrightarrow{}  Top  BY
                                                (RepUR  ``record``  3  THEN  Auto))
                        THEN  Repeat  (  RecordPlusTypeCD  THENL  [Id;  Auto]))\mcdot{})
  THEN  Auto)

---

Home Index