---

Step * of Lemma record-select_wf2

∀[T:𝕌']. ∀[z:Atom]. ∀[B:T ⟶ 𝕌']. ∀[r:Tz:B[self]].  (r.z ∈ B[r])
BY
{ ((Intros THEN Try ((At ⌜𝕌'⌝ (D 0)⋅ THEN Auto)))
   THEN D -1
   THEN Unfold `record-select` 0
   THEN DoSubsume
   THEN Auto
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[T:\mBbbU{}'].  \mforall{}[z:Atom].  \mforall{}[B:T  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[r:Tz:B[self]].    (r.z  \mmember{}  B[r])


By

---

Latex:
((Intros  THEN  Try  ((At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))
  THEN  D  -1
  THEN  Unfold  `record-select`  0
  THEN  DoSubsume
  THEN  Auto
  THEN  AutoSplit)

---

Home Index