---

Step * 1 of Lemma id-sdata-has-atom


1. x : Id
2. b : Atom1
3. True
⊢ b#data(x):SecurityData
BY
{ (Unfold `id-sdata` 0 THEN FreeFromAtomApElim_aux (Try (Unfold `sdata` 0)) ⌜x⌝⋅) }

---

Latex:

---

Latex:

1.  x  :  Id
2.  b  :  Atom1
3.  True
\mvdash{}  b\#data(x):SecurityData


By

---

Latex:
(Unfold  `id-sdata`  0  THEN  FreeFromAtomApElim\_aux  (Try  (Unfold  `sdata`  0))  \mkleeneopen{}x\mkleeneclose{}\mcdot{})

---

Home Index