---

Step * of Lemma es-E-mk-extended-eo

∀[Info,E:Type]. ∀[dom:E ⟶ 𝔹]. ∀[l:E ⟶ Id]. ∀[R:E ⟶ E ⟶ ℙ]. ∀[locless:E ⟶ E ⟶ 𝔹]. ∀[pred:E ⟶ E]. ∀[rank:E ⟶ ℕ].
∀[info:E ⟶ Info].
  ∀x:E. ((x ∈ E) ∧ (↑(dom x)))
BY
{ (RepeatFor 8 (Intro) THEN RepUR ``es-E mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,E:Type].  \mforall{}[dom:E  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[l:E  {}\mrightarrow{}  Id].  \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[locless:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[pred:E  {}\mrightarrow{}  E].  \mforall{}[rank:E  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[info:E  {}\mrightarrow{}  Info].
    \mforall{}x:E.  ((x  \mmember{}  E)  \mwedge{}  (\muparrow{}(dom  x)))


By

---

Latex:
(RepeatFor  8  (Intro)  THEN  RepUR  ``es-E  mk-extended-eo  mk-eo  mk-eo-record``  0  THEN  Auto)

---

Home Index