---

Step * of Lemma eo-record-type_wf

∀r:eo_record{i:l}(). (eo-record-type{i:l}(r) ∈ Atom ⟶ 𝕌')
BY
{ ((D 0 THENA Auto) THEN DRecord 1 THEN Auto THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}r:eo\_record\{i:l\}().  (eo-record-type\{i:l\}(r)  \mmember{}  Atom  {}\mrightarrow{}  \mBbbU{}')


By

---

Latex:
((D  0  THENA  Auto)  THEN  DRecord  1  THEN  Auto  THEN  ProveWfLemma)

---

Home Index