---

Step * 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 
⊢ r ∈ x:Atom ⟶ if x =a z then B[r] else T[x] fi 
BY
{ ((ExtWith [`u'] [⌜x:Atom ⟶ T[x]⌝]⋅ THENA Auto) THEN AutoSplit) }

1
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]

---

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 
\mvdash{}  r  \mmember{}  x:Atom  {}\mrightarrow{}  if  x  =a  z  then  B[r]  else  T[x]  fi 


By

---

Latex:
((ExtWith  [`u']  [\mkleeneopen{}x:Atom  {}\mrightarrow{}  T[x]\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  AutoSplit)

---

Home Index