---

Step * of Lemma record+_record

∀[T:Atom ⟶ 𝕌']. ∀[B:record(x.T[x]) ⟶ 𝕌']. ∀[z:Atom]. ∀[r:record(x.T[x])
                                                           z:B[self]].
  (r ∈ record(x.if x =a z then B[r] else T[x] fi ))
BY
{ ((Intros THEN Try ((At ⌜𝕌'⌝ (D 0)⋅ THEN Auto)))
   THEN Unfold `record+` -1
   THEN DepIsectHD (-1)
   THEN All (Unfold `record`)) }

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 
⊢ r ∈ x:Atom ⟶ if x =a z then B[r] else T[x] 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]].
    (r  \mmember{}  record(x.if  x  =a  z  then  B[r]  else  T[x]  fi  ))


By

---

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

---

Home Index