---

Step * of Lemma es-info-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.info(x)) = info ∈ (E ⟶ Info))
BY
{ (RepeatFor 9 (Intro) THEN RepUR ``es-info mk-extended-eo`` 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].
    ((\mlambda{}x.info(x))  =  info)


By

---

Latex:
(RepeatFor  9  (Intro)  THEN  RepUR  ``es-info  mk-extended-eo``  0  THEN  Auto)

---

Home Index