---

Step * of Lemma mk-eo-record_wf

∀[E:Type]. ∀[dom:E ─→ 𝔹]. ∀[l:E ─→ Id]. ∀[R:E ─→ E ─→ ℙ]. ∀[locless:E ─→ E ─→ 𝔹]. ∀[pred:E ─→ E]. ∀[rank:E ─→ ℕ].
  (mk-eo-record(E;dom;l;R;locless;pred;rank) ∈ eo_record{i:l}())
BY
{ (Auto
   THEN RepUR ``mk-eo-record eo_record`` 0
   THEN RepeatFor 7 ((RecordPlusTypeCD THEN Reduce 0 THEN Try (Trivial)))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:


\mforall{}[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{}].
    (mk-eo-record(E;dom;l;R;locless;pred;rank)  \mmember{}  eo\_record\{i:l\}())


By

(Auto
  THEN  RepUR  ``mk-eo-record  eo\_record``  0
  THEN  RepeatFor  7  ((RecordPlusTypeCD  THEN  Reduce  0  THEN  Try  (Trivial)))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index