---

Step * of Lemma id-sdata-has-atom

∀[x:Id]. ∀[b:Atom1].  uiff(b#data(x):SecurityData;True)
BY
{ At ⌜Type⌝ Auto⋅ }

1
1. x : Id
2. b : Atom1
3. True
⊢ b#data(x):SecurityData

---

Latex:

---

Latex:
\mforall{}[x:Id].  \mforall{}[b:Atom1].    uiff(b\#data(x):SecurityData;True)


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  Auto\mcdot{}

---

Home Index