---

Step * of Lemma trivial-record-update

∀[r,z:Top].  (r[z := r.z] ~ λx.if x =a z then r x else r x fi )
BY
{ ((UnivCD THENA Auto)
   THEN RW (BasicSymbolicComputeC []) 0
   THEN EqCD
   THEN RenameVar `a' (-1)
   THEN (InstLemma `atom_eq_sq_normalize` [⌜λ2z.r z⌝;⌜r a⌝;⌜a⌝;⌜z⌝]⋅ THENA Auto)
   THEN RevHypSubst (-1) 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r,z:Top].    (r[z  :=  r.z]  \msim{}  \mlambda{}x.if  x  =a  z  then  r  x  else  r  x  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (BasicSymbolicComputeC  [])  0
  THEN  EqCD
  THEN  RenameVar  `a'  (-1)
  THEN  (InstLemma  `atom\_eq\_sq\_normalize`  [\mkleeneopen{}\mlambda{}\msubtwo{}z.r  z\mkleeneclose{};\mkleeneopen{}r  a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RevHypSubst  (-1)  0\mcdot{}
  THEN  Auto)

---

Home Index