---

Step * of Lemma identity-record+-update

∀[T:Atom ⟶ 𝕌']. ∀[B:record(x.T[x]) ⟶ 𝕌']. ∀[z:Atom]. ∀[r:record(x.T[x])
                                                           z:B[self]]. ∀[x:Atom].
  (r[x := r.x] = r ∈ record(x.T[x])z:B[self])
BY
{ ((Intros THEN Try ((At ⌜𝕌'⌝ (D 0)⋅ THEN Auto)))
   THEN Unfold `record+` 0
   THEN DepIsectCD
   THEN Try ((BLemma `identity-record-update` THEN Auto))
   THEN (D 4 THEN Try (Trivial) THEN ExtWith [`a'] [x:Atom ⟶ T[x] ]⋅)
   THEN Try (Fold `record` 0)
   THEN Try (Complete (Auto))
   THEN AutoSplit
   THEN HypSubst' (-1) 0
   THEN RepUR ``record-update`` 0
   THEN RepeatFor 2 (Thin (-1))) }

1
1. T : Atom ⟶ 𝕌'
2. B : record(x.T[x]) ⟶ 𝕌'
3. z : Atom
4. r : self:record(x.T[x]) ⋂ x:Atom ⟶ if x =a z then B[self] else Top fi 
5. r ∈ record(x.T[x])
6. r ∈ x:Atom ⟶ if x =a z then B[r] else Top fi 
7. x : Atom
⊢ if z =a x then r.x else r z fi  = (r z) ∈ B[λz.if z =a x then r.x else r z fi ]

---

Latex:

---

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


By

---

Latex:
((Intros  THEN  Try  ((At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))
  THEN  Unfold  `record+`  0
  THEN  DepIsectCD
  THEN  Try  ((BLemma  `identity-record-update`  THEN  Auto))
  THEN  (D  4  THEN  Try  (Trivial)  THEN  ExtWith  [`a']  [x:Atom  {}\mrightarrow{}  T[x]  ]\mcdot{})
  THEN  Try  (Fold  `record`  0)
  THEN  Try  (Complete  (Auto))
  THEN  AutoSplit
  THEN  HypSubst'  (-1)  0
  THEN  RepUR  ``record-update``  0
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index