---

Step * 1 1 of Lemma record+_record


1. T : Atom ⟶ 𝕌'
2. B : (x:Atom ⟶ T[x]) ⟶ 𝕌'
3. z : Atom
4. r : self:x:Atom ⟶ T[x] ⋂ x:Atom ⟶ if x =a z then B[self] else Top fi 
5. r ∈ x:Atom ⟶ T[x]
6. r ∈ x:Atom ⟶ if x =a z then B[r] else Top fi 
7. u : Atom
8. u ≠ z ∈ Atom 
⊢ r u ∈ T[u]
BY
{ (Thin (-3)⋅ THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Atom  {}\mrightarrow{}  \mBbbU{}'
2.  B  :  (x:Atom  {}\mrightarrow{}  T[x])  {}\mrightarrow{}  \mBbbU{}'
3.  z  :  Atom
4.  r  :  self:x:Atom  {}\mrightarrow{}  T[x]  \mcap{}  x:Atom  {}\mrightarrow{}  if  x  =a  z  then  B[self]  else  Top  fi 
5.  r  \mmember{}  x:Atom  {}\mrightarrow{}  T[x]
6.  r  \mmember{}  x:Atom  {}\mrightarrow{}  if  x  =a  z  then  B[r]  else  Top  fi 
7.  u  :  Atom
8.  u  \mneq{}  z  \mmember{}  Atom 
\mvdash{}  r  u  \mmember{}  T[u]


By

---

Latex:
(Thin  (-3)\mcdot{}  THEN  DoSubsume  THEN  Auto)

---

Home Index